born_weight_pos
plain-language theorem explainer
The born weight, defined as the exponential of the negative recognition action for an outcome, is strictly positive for every real input. Researchers formalizing the gravity-coherence bridge would cite this to ensure Born-rule probabilities are well-defined and non-negative. The proof is a one-line wrapper applying the standard positivity theorem for the real exponential.
Claim. For every real number $C_I$, the born weight $w_I = e^{-C_I}$ satisfies $0 < w_I$.
background
The Coherence Collapse module formalizes the bridge from gravitational collapse to quantum measurement. Recognition action $C$ is the integral of J-cost along a path, residual rate action $A$ equals $-$ln(sin $θ_s$) for geodesic separation angle $θ_s$, and the central identity states $C = 2A$. Under this identity the born weight for outcome $I$ becomes $w_I = e^{-2A} = sin^2 θ_s = |α_I|^2$, recovering the Born rule $P(I) = |α_I|^2$ with mesoscopic thresholds near 0.2 ng and 1 s.
proof idea
The proof is a one-line wrapper that applies Real.exp_pos to the definition born_weight (C_I : ℝ) := Real.exp (-C_I). No unfolding, case split, or additional lemmas are required.
why it matters
This result supplies the born_positive field inside coherence_collapse_cert, the top-level certificate for the full coherence-collapse construction. It guarantees that the weights derived from the C = 2A identity remain positive so that the subsequent normalization step produces a valid probability distribution. The theorem therefore closes a necessary positivity condition for the Born-rule emergence claimed in the gravity-coherence paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.