rateAction_pos
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not compute a numerical value for the rate action.
- Does not extend the inequality to angles outside (0, π/2).
- Does not derive the Born rule, only a positivity property of the action.
- Does not address multi-branch or higher-dimensional cases.
formal statement (Lean)
41lemma rateAction_pos (rot : TwoBranchRotation) : 0 < rateAction rot := by
proof body
Tactic-mode proof.
42 unfold rateAction
43 apply neg_pos.mpr
44 have ⟨h1, h2⟩ := rot.θ_s_bounds
45 have hsin_pos : 0 < Real.sin rot.θ_s :=
46 sin_pos_of_pos_of_lt_pi h1 (by linarith : rot.θ_s < π)
47 -- sin θ < 1 for 0 < θ < π/2
48 have hsin_lt_one : Real.sin rot.θ_s < 1 := by
49 have hx1 : -(π / 2) ≤ rot.θ_s := by linarith
50 have hlt : rot.θ_s < π / 2 := h2
51 have : Real.sin rot.θ_s < Real.sin (π / 2) :=
52 sin_lt_sin_of_lt_of_le_pi_div_two hx1 le_rfl hlt
53 simpa [Real.sin_pi_div_two] using this
54 exact Real.log_neg hsin_pos hsin_lt_one
55
56/-- Born weight from rate action: exp(-2A) = sin²(θ_s) -/