m_coh_positive
plain-language theorem explainer
The theorem asserts positivity of the coherence mass threshold in SI units. Optomechanics and quantum gravity researchers cite it when locating the scale separating persistent superpositions from rapid decoherence. The proof reduces to unfolding the constant definition 2e-13 and applying normalization.
Claim. $0 < m_ {coh}$ where $m_{coh} = 2e-13$ kg is the mass at which residual action $A$ reaches order unity for coherence time near 1 s.
background
The module develops the C = 2A identity that links gravitational collapse to the Born rule via recognition cost. Recognition action integrates J-cost along a path while residual rate action equals -ln(sin θ_s) for geodesic separation angle θ_s. The central claim equates recognition action to twice the residual action, yielding Born probabilities as normalized exponentials of the costs.
proof idea
The proof is a one-line wrapper that unfolds the definition m_coh_kg := 2e-13 and applies norm_num to verify the strict inequality for this positive real.
why it matters
The result fixes the mesoscopic threshold inside the coherence-collapse framework, placing the A ≈ 1 transition at an experimentally accessible nanogram scale. It supplies the concrete mass value presupposed by the C = 2A identity and the Born-rule emergence statements in the module. No downstream theorems depend on it yet; the declaration simply discharges the basic positivity obligation for the gravity-coherence paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.