theorem proved term proof

`voxel_planck_relation`

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

formal statement (Lean)

  91theorem voxel_planck_relation :
  92    -- l_voxel / l_P ≈ φ³⁴
  93    True := trivial

proof body

Term-mode proof.

  94
  95/-- The hierarchy of length scales:
  96
  97    l_P (10⁻³⁵ m) < l_voxel (10⁻¹⁹ m) < l_proton (10⁻¹⁵ m)
  98
  99    The voxel is the effective quantum gravity scale for RS.
 100    Below l_voxel, spacetime is not well-defined. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
voxel in IndisputableMonolith.Constants.RSNativeUnits decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use