rateAction_pos
plain-language theorem explainer
The lemma shows that the rate action A = -ln(sin θ_s) is strictly positive whenever the starting angle of a two-branch rotation satisfies 0 < θ_s < π/2. Measurement theorists using geodesic models of collapse would cite it to guarantee that the derived Born weight lies strictly between zero and one. The proof unfolds the definition and reduces the claim to the standard inequalities 0 < sin θ_s < 1 on that interval, followed by the negativity of the logarithm.
Claim. Let rot be a two-branch rotation with starting angle θ_s satisfying 0 < θ_s < π/2. Then the rate action A = -ln(sin θ_s) satisfies A > 0.
background
The module formalizes two-branch quantum measurement geometry on the Bloch sphere. A TwoBranchRotation is a structure carrying a starting angle θ_s together with the bounds 0 < θ_s < π/2 and a positive duration T. The rate action is defined by A = -ln(sin θ_s). The module states that the residual norm equals π/2 - θ_s and that the Born weight is given by exp(-2A) = sin²(θ_s) = |α₂|².
proof idea
The proof unfolds rateAction to -log(sin θ_s) and applies neg_pos.mpr. It extracts the bounds from the rotation structure, invokes sin_pos_of_pos_of_lt_pi to obtain sin θ_s > 0, and uses sin_lt_sin_of_lt_of_le_pi_div_two with sin(π/2) = 1 to obtain sin θ_s < 1. The final step applies Real.log_neg.
why it matters
The result supplies the positivity needed to ensure the Born weight derived from the rate action is strictly between zero and one. It supports the geodesic interpretation of the two-branch measurement in Local-Collapse §3. The lemma sits inside the measurement layer and does not yet link to the forcing chain or the phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.