rateAction_pos
open lean source
IndisputableMonolith.Measurement.TwoBranchGeodesic on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
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.
depends on
formal source
38 - Real.log (Real.sin rot.θ_s)
39
40/-- Rate action is positive for θ_s ∈ (0, π/2) -/
41lemma rateAction_pos (rot : TwoBranchRotation) : 0 < rateAction rot := by
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) -/
57theorem born_weight_from_rate (rot : TwoBranchRotation) :
58 Real.exp (- 2 * rateAction rot) = (Real.sin rot.θ_s) ^ 2 := by
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 -/