born_weight_from_rate
The theorem equates exp(-2A) to sin²(θ_s) for any two-branch rotation, where A denotes the rate action. Quantum measurement modelers cite it to derive Born-rule weights directly from geodesic rate actions in the two-branch setting. The proof substitutes the rate-action definition and reduces via logarithm and exponential identities after verifying positivity of the sine.
claimFor a two-branch rotation with starting angle θ_s ∈ (0, π/2), exp(-2A) = sin²(θ_s) where the rate action A is defined by A = -ln(sin θ_s).
background
The module develops the two-branch quantum measurement geodesic. A TwoBranchRotation is a structure carrying a starting angle θ_s (0 < θ_s < π/2), a positive duration T, and the associated bounds. The rate action is the auxiliary definition A = -ln(sin θ_s), taken from equation (4.7) of Local-Collapse; the residual geodesic length is π/2 - θ_s. The upstream PrimitiveDistinction supplies the seven-axiom foundation that yields the four structural conditions used here.
proof idea
Unfold rateAction to replace A by -log(sin θ_s). The θ_s bounds give sin θ_s > 0 via sin_pos_of_pos_of_lt_pi. The subsequent calc applies ring_nf to the exponent, rewrites the argument via log_pow, and finishes with exp_log on the positive quantity sin² θ_s.
why it matters in Recognition Science
weight_equals_born invokes the result to equate path weight with initial amplitude squared; C_equals_2A uses it to exhibit C = 2A with exp(-C) matching the squared amplitude. The equality therefore supplies the direct link from rate action to Born weight inside the two-branch geodesic, advancing the measurement bridge toward the Recognition framework's T5–T8 chain and the RCL composition law.
scope and limits
- Does not derive the Born rule for measurements outside the two-branch geometry.
- Does not compute rate actions for rotations with θ_s outside (0, π/2).
- Does not address normalization across multiple branches or full state evolution.
- Does not incorporate time-dependent dynamics beyond the fixed rotation duration T.
Lean usage
have h := born_weight_from_rate rotformal statement (Lean)
57theorem born_weight_from_rate (rot : TwoBranchRotation) :
58 Real.exp (- 2 * rateAction rot) = (Real.sin rot.θ_s) ^ 2 := by
proof body
Tactic-mode proof.
59 unfold rateAction
60 -- exp(-2*(-log(sin θ))) = exp(2 log(sin θ))
61 have ⟨h1, h2⟩ := rot.θ_s_bounds
62 have hsin_pos : 0 < Real.sin rot.θ_s :=
63 sin_pos_of_pos_of_lt_pi h1 (by linarith : rot.θ_s < π)
64 calc Real.exp (- 2 * (- Real.log (Real.sin rot.θ_s)))
65 = Real.exp (2 * Real.log (Real.sin rot.θ_s)) := by ring_nf
66 _ = Real.exp (Real.log ((Real.sin rot.θ_s) ^ 2)) := by
67 congr 1
68 exact (Real.log_pow (Real.sin rot.θ_s) 2).symm
69 _ = (Real.sin rot.θ_s) ^ 2 := Real.exp_log (pow_pos hsin_pos 2)
70
71/-- Initial amplitude |α₂|² = sin²(θ_s) from geometry -/