Documentation Verification Report

SpeedOfLight

📁 Source: PhysLean/Relativity/SpeedOfLight.lean

Statistics

Metric	Count
Definitions `SpeedOfLight`, `instCoeReal`, `instOne`, `val`	4
Theorems `pos`, `val_ne_zero`, `val_nonneg`, `val_one`, `val_pos`	5
Total	9

SpeedOfLight

Definitions

Name	Category	Theorems
`instCoeReal` 📖	CompOp	—
`instOne` 📖	CompOp	1 math math: `val_one`
`val` 📖	CompOp	83 math math: `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField`, `SpaceTime.distTimeSlice_distDeriv_inl`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField`, `Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction_eq_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ_time_deriv`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq`, `Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate`, `Electromagnetism.FreeSpace.c_abs`, `SpaceTime.toTimeAndSpace_symm_measurePreserving`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_time_deriv`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ`, `SpaceTime.distTimeSlice_symm_distTimeDeriv_eq`, `SpaceTime.spaceTime_integral_eq_time_space_integral`, `SpaceTime.deriv_sum_inl`, `val_nonneg`, `Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate`, `Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ'`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ`, `Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ`, `SpaceTime.toTimeAndSpace_basis_inl'`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv_eq_time_deriv`, `SpaceTime.time_val_toCoord_symm`, `pos`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_electricField_eq_magneticFieldMatrix`, `SpaceTime.boost_zero_apply_time_space`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_electricField_eq_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_magneticFunction`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_succ_zero`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_eq_electricField`, `SpaceTime.det_timeSpaceBasisEquiv`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_electricFunction`, `SpaceTime.timeSpaceBasis_addHaar`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0`, `SpaceTime.toTimeAndSpace_symm_apply_inl`, `Electromagnetism.FreeSpace.c_val`, `Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_time_deriv`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate`, `SpaceTime.spaceTime_integral_eq_space_integral_time_integral`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate`, `Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix`, `Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ_space_deriv_zero`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero`, `Electromagnetism.LorentzCurrentDensity.chargeDensity_eq_timeSlice`, `Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema`, `SpaceTime.spaceTime_integral_eq_time_integral_space_integral`, `val_pos`, `SpaceTime.distDeriv_inl_distTimeSlice_symm`, `Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv_eq_time_deriv`, `SpaceTime.toTimeAndSpace_basis_inl`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `Electromagnetism.FreeSpace.c_sq`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero`, `Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity`, `Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ`, `SpaceTime.timeSpaceBasis_apply_inl`, `val_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pos` 📖	mathematical	—	`val`	—	—
`val_ne_zero` 📖	—	—	—	—	`pos`
`val_nonneg` 📖	mathematical	—	`val`	—	`pos`
`val_one` 📖	mathematical	—	`val` `SpeedOfLight` `instOne`	—	—
`val_pos` 📖	mathematical	—	`val`	—	`pos`

(root)

Definitions

Name	Category	Theorems
`SpeedOfLight` 📖	CompData	1 math math: `SpeedOfLight.val_one`

---

← Back to Index