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)
121theorem m_coh_nanogram_range : m_coh_kg < 1e-9 ∧ m_coh_kg > 1e-15 := by
proof body
Term-mode proof.
122 unfold m_coh_kg; constructor <;> norm_num
123
124/-! ## Distinguishing Predictions -/
125
126/-- RS prediction: collapse rate PLATEAUS after orthogonality (A → const).
127 Penrose-Diósi: collapse rate continues growing with 1/d tail.
128 This is a sharp distinguisher. -/
depends on (10)
Lean names referenced from this declaration's body.
-
const
in IndisputableMonolith.Action.PathSpace
decl_use
-
sharp
in IndisputableMonolith.Cost.Ndim.Projector
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
m_coh_kg
in IndisputableMonolith.Gravity.CoherenceCollapse
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use