theorem proved term proof

`lambda_kin_eq_K_gate_ratio`

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

formal statement (Lean)

 227theorem lambda_kin_eq_K_gate_ratio :
 228    lambda_kin = Constants.RSUnits.K_gate_ratio := by

proof body

Term-mode proof.

 229  unfold lambda_kin
 230  have hlog : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
 231  simp [Constants.RSUnits.lambda_kin_display, Constants.RSUnits.K_gate_ratio, U, voxel]
 232  field_simp [hlog]
 233  ring
 234
 235/-! ## Planck-Scale Quantities (RS-derived)
 236
 237In RS, the Planck scale emerges from the gate identities, not as a postulate.
 238These are expressed in RS-native units.
 239-/
 240
 241/-- Planck time in RS units: τ_P = √(ħG/c⁵).
 242    In RS-native units, this is a dimensionless φ-expression. -/

depends on (24)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
one_lt_phi in IndisputableMonolith.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
K_gate_ratio in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_display in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin in IndisputableMonolith.Constants.RSNativeUnits decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
voxel in IndisputableMonolith.Constants.RSNativeUnits decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use
emerges in IndisputableMonolith.RecogGeom.Comparative decl_use
U in IndisputableMonolith.Recognition decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use