Measurement Two Branch Geodesic Rate Action Pos

The rate action

In quantum mechanics, a measurement with two possible outcomes is often pictured as a rotation on the Bloch sphere, the standard geometric representation of a two-state system. The Recognition Science framework formalizes one such rotation as a two-branch rotation: a starting angle θ_s between 0 and π/2, and a duration T that is positive. The starting angle encodes the initial amplitudes of the two branches, and the rotation carries the state to the measurement axis.

From this geometry, the framework defines the rate action A = -ln(sin θ_s). This is a single number derived from the starting angle, and it measures how much "action" is packed into the rotation. The declaration rateAction_pos is a machine-checked proof that this number is always positive: for any allowed starting angle, A > 0. The proof follows directly from the fact that sin θ_s lies strictly between 0 and 1 when θ_s is in the open interval (0, π/2), so its natural logarithm is negative, and the minus sign makes the action positive.

The positivity matters because the rate action feeds directly into the Born rule, the standard quantum rule that converts amplitudes into probabilities. The framework proves that the weight of one branch is exp(-2A) = sin²(θ_s), which is exactly the squared amplitude of that branch. Since A is positive, this weight is a number between 0 and 1, and the complementary branch has weight cos²(θ_s). The two weights sum to 1, as probabilities must, and this normalization is also a proved theorem in the same module.

In Recognition Science, this chain of definitions and proofs shows that the Born rule's probability structure is not an added assumption but a consequence of the rotation geometry. The rate action is the bridge: a positive, well-defined quantity that converts a geometric starting angle into a probability weight. The framework's library, a machine-checked collection of formal theorems, records this as a lemma about the rate action, not as a physical claim about how measurements actually occur in the laboratory.

/-- Rate action is positive for θ_s ∈ (0, π/2) -/
lemma rateAction_pos (rot : TwoBranchRotation) : 0 < rateAction rot := by
  unfold rateAction
  apply neg_pos.mpr
  have ⟨h1, h2⟩ := rot.θ_s_bounds
  have hsin_pos : 0 < Real.sin rot.θ_s :=
    sin_pos_of_pos_of_lt_pi h1 (by linarith : rot.θ_s < π)
  -- sin θ < 1 for 0 < θ < π/2
  have hsin_lt_one : Real.sin rot.θ_s < 1 := by
    have hx1 : -(π / 2) ≤ rot.θ_s := by linarith
    have hlt : rot.θ_s < π / 2 := h2
    have : Real.sin rot.θ_s < Real.sin (π / 2) :=
      sin_lt_sin_of_lt_of_le_pi_div_two hx1 le_rfl hlt
    simpa [Real.sin_pi_div_two] using this
  exact Real.log_neg hsin_pos hsin_lt_one

/-- Born weight from rate action: exp(-2A) = sin²(θ_s) -/
theorem born_weight_from_rate (rot : TwoBranchRotation) :
  Real.exp (- 2 * rateAction rot) = (Real.sin rot.θ_s) ^ 2 := by
  unfold rateAction
  -- exp(-2*(-log(sin θ))) = exp(2 log(sin θ))
  have ⟨h1, h2⟩ := rot.θ_s_bounds
  have hsin_pos : 0 < Real.sin rot.θ_s :=
    sin_pos_of_pos_of_lt_pi h1 (by linarith : rot.θ_s < π)
  calc Real.exp (- 2 * (- Real.log (Real.sin rot.θ_s)))
      = Real.exp (2 * Real.log (Real.sin rot.θ_s)) := by ring_nf
      _ = Real.exp (Real.log ((Real.sin rot.θ_s) ^ 2)) := by
        congr 1
        exact (Real.log_pow (Real.sin rot.θ_s) 2).symm
      _ = (Real.sin rot.θ_s) ^ 2 := Real.exp_log (pow_pos hsin_pos 2)

/-- Amplitudes sum to 1 (normalization) -/
theorem amplitudes_normalized (rot : TwoBranchRotation) :
  initialAmplitudeSquared rot + complementAmplitudeSquared rot = 1 := by
  unfold initialAmplitudeSquared complementAmplitudeSquared
  exact Real.sin_sq_add_cos_sq rot.θ_s

What this page does not claim

This proof does not claim that the two-branch rotation model describes actual physical measurements in the laboratory. It does not claim that the rate action is the only quantity governing measurement outcomes. It does not claim that the starting angle θ_s is determined by any physical law within this module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/TwoBranchGeodesic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: