born_weight_is_sin_sq
plain-language theorem explainer
The declaration establishes that under the C equals 2A relation the born weight of a recognition action at separation angle theta_s equals sin squared of theta_s when the sine is positive. Researchers deriving the Born rule from gravitational coherence collapse would cite this identity. The proof reduces the expression by unfolding the action definitions then applying logarithm power rules followed by the exponential of log identity.
Claim. For the case where recognition action equals twice residual action, the born weight of the recognition action at separation angle $theta_s$ equals $sin^2 theta_s$, provided $sin theta_s > 0$.
background
In the Coherence Collapse module the recognition action is the integral of J-cost along a path while residual rate action A equals negative log of sin theta_s for geodesic separation angle theta_s. The central relation C equals 2A connects gravitational collapse to quantum measurement. Upstream the probability definition in QuantumLedger gives the Born rule as squared norm of amplitudes which this theorem helps derive from the exponential of negative costs. The module formalizes the bridge between gravitational coherence and the Born rule via recognition costs.
proof idea
The proof unfolds the definitions of born_weight, recognition_action and rate_action. It rewrites the negative log expression using ring to simplify to twice the log of sin theta_s, applies the log of power rule, and finally uses the exp_log lemma on the positive square to recover sin squared theta_s.
why it matters
This result fills the central identity C equals 2A in the gravity-coherence paper enabling the emergence of the Born rule as probability equals exp of negative C over sum exp of negative C equals absolute alpha squared. It connects to the Recognition Science framework through the J-cost and phi-forcing structures. The theorem supports the mesoscopic threshold calculations for coherence masses around 0.2 ng.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.