born_weight_from_rate
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.