m_coh_kg
plain-language theorem explainer
The definition supplies the numerical value 2e-13 kg for the mesoscopic mass threshold at which residual action A reaches order unity for coherence times near one second. Optomechanical experimentalists testing gravity-induced decoherence would cite this scale when designing setups that probe the quantum-to-classical boundary. It is introduced as a direct constant assignment that satisfies the nanogram-range bounds required by the coherence certificate.
Claim. $m_ {coh} = 2 times 10^{-13}$ kg, the mass at which the residual action $A$ reaches order one for coherence times of order one second, marking the transition from persistent quantum superpositions to rapid decoherence.
background
The module formalizes the C = 2A identity that connects gravitational collapse to quantum measurement via recognition cost. Recognition action is the integral of the J-cost along a path; residual rate action equals -ln(sin theta_s) for geodesic separation angle theta_s. The central identity states that recognition action equals twice the residual action, from which the Born rule emerges as the normalized exponential of the negative costs.
proof idea
Direct constant definition with no proof obligations.
why it matters
This constant supplies the numerical threshold required by the CoherenceCollapseCert structure, which certifies that C = 2A, Born weights are positive and normalized, and the threshold lies in the nanogram range. It distinguishes RS predictions of a plateau after orthogonality from Penrose-Diósi models that continue growing. The value aligns with the mesoscopic scale in the gravity-coherence paper where optomechanical tests become feasible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.