Measurement Two Branch Geodesic Residual Action Invariant

The residual action

In the two-branch model of quantum measurement, a state starts at an angle θ_s between 0 and π/2 and rotates to the measurement outcome at π/2. The residual action, a discrete record of the remaining rotation, is defined as S = π/2 − θ_s, the geodesic length on the Bloch sphere. The declaration residual_action_invariant proves that this residual action equals π/2 − θ_s by definition, and because the definition contains no time variable, the value is invariant under reparameterization of the rotation's duration. In plain terms: the remaining angular distance to the outcome is fixed by the starting angle alone, no matter how the rotation is timed.

The framework's machine-checked library of formal theorems also shows what follows from this geometry. The rate action A = −ln(sin θ_s) is positive for all allowed starting angles, and the Born weight exp(−2A) equals sin²(θ_s), which matches the initial amplitude |α₂|². The two branch amplitudes, sin²(θ_s) and cos²(θ_s), sum to 1, so the model respects normalization. These results are proved in the library, not assumed.

What the declaration does not claim: it does not assert that any physical measurement actually follows this two-branch rotation. It only establishes a mathematical identity about a defined quantity. It also does not claim that the residual action is the only action in the theory, nor that the reparameterization invariance extends to other quantities such as the rate action, which depends explicitly on the angle but not on time either. The theorem is a definitional equality, not a physical law.

/-- Residual action S = π/2 - θ_s (geodesic length on Bloch sphere) -/
noncomputable def residualAction (rot : TwoBranchRotation) : ℝ :=
  π/2 - rot.θ_s

/-- The geodesic is independent of time parameterization (reparameterization invariance) -/
theorem residual_action_invariant (rot : TwoBranchRotation) :
  residualAction rot = π/2 - rot.θ_s := rfl

/-- 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

The declaration does not claim that real quantum measurements follow this two-branch rotation. The declaration does not claim that the residual action is the only action in the theory. The declaration does not claim that reparameterization invariance applies to the rate action.

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: