lemma proved term proof

`c_ell0_tau0`

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

formal statement (Lean)

 420lemma c_ell0_tau0 : c * tau0 = ell0 := by

proof body

Term-mode proof.

 421  simp [c, tau0, ell0, tick]
 422
 423/-- Fundamental recognition wavelength λ_rec.
 424    In the 8-tick cycle, λ_rec = ℓ₀ (in RS-native units). -/

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

UnitsKGateCert in IndisputableMonolith.Certificates.UnitsKGate decl_use
RSUnits in IndisputableMonolith.Constants decl_use
ell0_div_tau0_eq_c in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_units_invariant in IndisputableMonolith.Constants.KDisplay decl_use
observable_factors_through_quotient in IndisputableMonolith.Constants.KDisplay decl_use
lambda_kin_from_tau_rec in IndisputableMonolith.Constants.KDisplayCore decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
c_mul_tau0_eq_ell0 in IndisputableMonolith.Constants.RSUnitsHelpers decl_use
cone_bound in IndisputableMonolith.LightCone.StepBounds decl_use
cone_bound_saturates in IndisputableMonolith.LightCone.StepBounds decl_use
bh_entropy_from_ledger in IndisputableMonolith.Relativity.Compact.BlackHoleEntropy decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use
units_identity_holds in IndisputableMonolith.URCAdapters.UnitsIdentity decl_use

depends on (7)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use