theorem proved term proof

`display_null_condition`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 131theorem display_null_condition (U : RSUnits) (h : 0 < U.tau0) :
 132  ((lambda_kin_display U) / (tau_rec_display U))^2 = U.c^2 := by

proof body

Term-mode proof.

 133  simp only [display_speed_eq_c U h]
 134
 135/-! Bridge Coherence and Categorical Structure -/
 136
 137/-- Units equivalence class: two units packs are equivalent if they have same c -/

depends on (14)

Lean names referenced from this declaration's body.

Structure in IndisputableMonolith.Chemistry.CrystalStructure decl_use
tau0 in IndisputableMonolith.Compat.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
display_speed_eq_c in IndisputableMonolith.Constants.KDisplay decl_use
lambda_kin_display in IndisputableMonolith.Constants.KDisplayCore decl_use
tau_rec_display in IndisputableMonolith.Constants.KDisplayCore decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use
U in IndisputableMonolith.Recognition decl_use
Bridge in IndisputableMonolith.RecogSpec.Core decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use