No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
129noncomputable def tau19 : ℝ := tau0 * phi^19
proof body
Definition body.
130
131/-! ## Quantum Gravity Predictions -/
132
133/-- RS predictions for quantum gravity:
134
135 1. **Minimum length = l_voxel**, not l_P
136 - Below l_voxel, spacetime is discrete
137 - l_P may be inaccessible
138
139 2. **φ-quantized energies** near Planck scale
140 - Energies at φ^n × E_P
141
142 3. **No singularities**
143 - Voxel structure prevents infinite densities
144
145 4. **Modified dispersion relations**
146 - At high energy, E² = p²c² + m²c⁴ + corrections -/
depends on (11)
Lean names referenced from this declaration's body.
-
tau0
in IndisputableMonolith.Compat.Constants
decl_use
-
tau0
in IndisputableMonolith.Constants
decl_use
-
tau0
in IndisputableMonolith.Constants.Derivation
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
dispersion
in IndisputableMonolith.Foundation.SimplicialLedger.LorentzEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Voxel
in IndisputableMonolith.Measurement.RSNative.Core
decl_use