born_weight_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute any explicit value of the recognition action $C_I$.
- Does not establish the C = 2A identity.
- Does not address summation or normalization over multiple outcomes.
- Does not derive the sin-squared representation of the weight.
formal statement (Lean)
83theorem born_weight_pos (C_I : ℝ) : 0 < born_weight C_I := Real.exp_pos _
proof body
Term-mode proof.
84
85/-- For the C = 2A case: born_weight = sin²(θ_s).
86 This follows from exp(-2A) = exp(2 ln sin θ) = sin²θ. -/