m_coh_nanogram_range
plain-language theorem explainer
The coherence mass threshold lies strictly between 10^{-15} and 10^{-9} kilograms. Optomechanical experimentalists would cite this bound when assessing accessibility of gravity-induced decoherence tests. The proof is a one-line term wrapper that unfolds the kilogram definition and verifies both sides of the conjunction by direct numerical normalization.
Claim. $10^{-15} < m_0 < 10^{-9}$ (kilograms), where $m_0$ is the mesoscopic coherence mass at which gravitational collapse becomes detectable via the recognition-action threshold.
background
The module formalizes the link between gravitational collapse and the Born rule through the identity C = 2A, where C is the recognition action obtained by integrating the J-cost along a path and A is the residual rate action measuring geodesic separation angle. The mesoscopic threshold is given as approximately 0.2 ng with coherence time near 1 s when A is order unity. Upstream, m_coh_kg supplies the explicit kilogram-scale expression obtained from the phi-ladder mass formula and the IntegrationGap.A edge count.
proof idea
The proof is a one-line term-mode wrapper. It unfolds m_coh_kg to expose the concrete numerical expression, splits the conjunction with constructor, and discharges both inequalities by norm_num.
why it matters
The result places the collapse threshold inside the nanogram window directly accessible to optomechanical experiments (Aspelmeyer, Romero-Isart). It supplies the concrete mass bound required by the C = 2A framework and the distinguishing prediction that collapse rate plateaus after orthogonality. The declaration closes the mesoscopic prediction step in the gravity-coherence development; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.