· ColorCenter Jill/Chemistry/ColorCenters.lean:41 structure
· nv_center Jill/Chemistry/ColorCenters.lean:62 def
· siv_center Jill/Chemistry/ColorCenters.lean:77 def
· gev_center Jill/Chemistry/ColorCenters.lean:91 def
· cr_corundum Jill/Chemistry/ColorCenters.lean:108 def
? siv_dw_gt_nv_dw Jill/Chemistry/ColorCenters.lean:126 theorem
? siv_dw_ratio_gt_17 Jill/Chemistry/ColorCenters.lean:133 theorem
? nv_qy_gt_siv_qy Jill/Chemistry/ColorCenters.lean:139 theorem
? nv_cr_brightest Jill/Chemistry/ColorCenters.lean:146 theorem
· defectQuantumYield Jill/Chemistry/ColorCenters.lean:156 def
? qy_nonneg Jill/Chemistry/ColorCenters.lean:161 theorem
? qy_le_one Jill/Chemistry/ColorCenters.lean:169 theorem
? qy_mono_kr Jill/Chemistry/ColorCenters.lean:178 theorem
? qy_antimono_knr Jill/Chemistry/ColorCenters.lean:192 theorem
· beerLambert Jill/Chemistry/ColorCenters.lean:205 def
? beerLambert_nonneg Jill/Chemistry/ColorCenters.lean:209 theorem
? beerLambert_le_I₀ Jill/Chemistry/ColorCenters.lean:216 theorem
? beerLambert_antimono_concentration Jill/Chemistry/ColorCenters.lean:229 theorem
? beerLambert_antimono_length Jill/Chemistry/ColorCenters.lean:242 theorem
· phononSidebandFraction Jill/Chemistry/ColorCenters.lean:256 def
? psb_nonneg Jill/Chemistry/ColorCenters.lean:259 theorem
? psb_le_one Jill/Chemistry/ColorCenters.lean:264 theorem
? dw_plus_psb Jill/Chemistry/ColorCenters.lean:269 theorem
? higher_dw_less_psb Jill/Chemistry/ColorCenters.lean:274 theorem
· stokesShift_nm Jill/Chemistry/ColorCenters.lean:283 def
? stokesShift_pos Jill/Chemistry/ColorCenters.lean:288 theorem
? nv_easier_to_form_than_siv Jill/Chemistry/ColorCenters.lean:297 theorem
? gev_highest_formation_energy Jill/Chemistry/ColorCenters.lean:303 theorem
· fluorescencePerTransmittedPhoton Jill/Chemistry/ColorCenters.lean:316 def
? fluorescence_per_photon_nonneg Jill/Chemistry/ColorCenters.lean:320 theorem
· OctahedralField Jill/Chemistry/CrystalField.lean:29 structure
· eg_energy Jill/Chemistry/CrystalField.lean:36 def
· t2g_energy Jill/Chemistry/CrystalField.lean:39 def
? total_splitting Jill/Chemistry/CrystalField.lean:42 theorem
? eg_above_barycenter Jill/Chemistry/CrystalField.lean:47 theorem
? t2g_below_barycenter Jill/Chemistry/CrystalField.lean:51 theorem
? barycenter_preserved Jill/Chemistry/CrystalField.lean:58 theorem
· tetrahedral_Dq Jill/Chemistry/CrystalField.lean:67 def
? tetrahedral_Dq_pos Jill/Chemistry/CrystalField.lean:70 theorem
? tetrahedral_lt_octahedral Jill/Chemistry/CrystalField.lean:75 theorem
? tetrahedral_total_splitting Jill/Chemistry/CrystalField.lean:81 theorem
· energyToWavelength Jill/Chemistry/CrystalField.lean:88 def
? energyToWavelength_pos Jill/Chemistry/CrystalField.lean:91 theorem
? higher_energy_shorter_wavelength Jill/Chemistry/CrystalField.lean:96 theorem
· RacahParams Jill/Chemistry/CrystalField.lean:106 structure
· dqOverB Jill/Chemistry/CrystalField.lean:113 def
? dqOverB_pos Jill/Chemistry/CrystalField.lean:116 theorem
· cfse_d3 Jill/Chemistry/CrystalField.lean:122 def
? cfse_d3_value Jill/Chemistry/CrystalField.lean:125 theorem
? cfse_d3_stabilizing Jill/Chemistry/CrystalField.lean:130 theorem
· ruby_field Jill/Chemistry/CrystalField.lean:139 def
· emerald_field Jill/Chemistry/CrystalField.lean:144 def
· alexandrite_field Jill/Chemistry/CrystalField.lean:150 def
? alexandrite_between Jill/Chemistry/CrystalField.lean:153 theorem
? ruby_stronger_field Jill/Chemistry/CrystalField.lean:161 theorem
? ruby_absorbs_green Jill/Chemistry/CrystalField.lean:166 theorem
? emerald_absorbs_red Jill/Chemistry/CrystalField.lean:174 theorem
· SpinCrossover Jill/Chemistry/CrystalField.lean:185 structure
· isHighSpin Jill/Chemistry/CrystalField.lean:194 def
· isLowSpin Jill/Chemistry/CrystalField.lean:197 def
? spin_exclusive Jill/Chemistry/CrystalField.lean:200 theorem
· NephelauxeticRatio Jill/Chemistry/CrystalField.lean:209 structure
· complexB Jill/Chemistry/CrystalField.lean:218 def
? complex_B_le_free Jill/Chemistry/CrystalField.lean:222 theorem
? complex_B_pos Jill/Chemistry/CrystalField.lean:228 theorem
· JahnTellerDistortion Jill/Chemistry/CrystalField.lean:238 structure
? jahn_teller_lowers_energy Jill/Chemistry/CrystalField.lean:248 theorem
· cfse_highspin_dq Jill/Chemistry/CrystalField.lean:256 def
? cfse_zero_shells Jill/Chemistry/CrystalField.lean:271 theorem
? cfse_d3_d8_maximal Jill/Chemistry/CrystalField.lean:279 theorem
? cfse_nonpositive Jill/Chemistry/CrystalField.lean:286 theorem
· cr_2E_state Jill/Chemistry/CrystalField.lean:299 def
? cr_2E_state_pos Jill/Chemistry/CrystalField.lean:302 theorem
? ruby_R_line_at_694nm Jill/Chemistry/CrystalField.lean:306 theorem
? cr_2E_below_4T2 Jill/Chemistry/CrystalField.lean:315 theorem
· CVDConditions Jill/Chemistry/Synthesis.lean:35 structure
· growthRate Jill/Chemistry/Synthesis.lean:56 def
? growthRate_pos Jill/Chemistry/Synthesis.lean:60 theorem
? growthRate_mono_temp Jill/Chemistry/Synthesis.lean:69 theorem
? growthRate_mono_methane Jill/Chemistry/Synthesis.lean:83 theorem
· nitrogenConcentration Jill/Chemistry/Synthesis.lean:99 def
? nitrogen_mono_source Jill/Chemistry/Synthesis.lean:103 theorem
? slower_growth_more_nitrogen Jill/Chemistry/Synthesis.lean:113 theorem
· sp3Fraction Jill/Chemistry/Synthesis.lean:126 def
? sp3_nonneg Jill/Chemistry/Synthesis.lean:130 theorem
? sp3_le_one Jill/Chemistry/Synthesis.lean:138 theorem
? sp3_mono_h2 Jill/Chemistry/Synthesis.lean:145 theorem
· HydrothermalConditions Jill/Chemistry/Synthesis.lean:155 structure
· quartz_min_temp_K Jill/Chemistry/Synthesis.lean:169 def
· quartz_min_pressure_MPa Jill/Chemistry/Synthesis.lean:170 def
· dissolutionRate Jill/Chemistry/Synthesis.lean:173 def
? dissolution_mono_temp Jill/Chemistry/Synthesis.lean:177 theorem
· CzochralskiConditions Jill/Chemistry/Synthesis.lean:191 structure
· segregationCoeff Jill/Chemistry/Synthesis.lean:205 def
· scheilConcentration Jill/Chemistry/Synthesis.lean:211 def
? segregation_pos Jill/Chemistry/Synthesis.lean:215 theorem
· synthesisCost Jill/Chemistry/Synthesis.lean:224 def
? cost_mono_time Jill/Chemistry/Synthesis.lean:228 theorem
? synthesis_time_from_rate Jill/Chemistry/Synthesis.lean:236 theorem
· cvdValidTempRange Jill/Chemistry/Synthesis.lean:257 def
+925 more — narrow with filters