Measurement Two Branch Geodesic

The two-branch geodesic

A geodesic is the shortest path between two points on a curved surface. On a sphere, geodesics are arcs of great circles, like the routes an airplane takes between continents. In quantum mechanics, the state of a two-level system, such as the spin of an electron, can be pictured as a point on a sphere called the Bloch sphere. A measurement that distinguishes two outcomes rotates this point from its initial position to the north pole, and the rotation traces an arc. The two-branch geodesic is that arc: the shortest, most direct rotation the measurement can perform.

The geometry is simple. The initial state sits at an angle θ_s measured from the north pole, where 0 < θ_s < π/2. The measurement rotates the state to the north pole, at angle π/2. The length of the geodesic is the difference, π/2 − θ_s. This length is called the residual action, and it is independent of how fast or how slowly the rotation happens. A slow rotation and a fast rotation trace the same arc, so the length does not depend on time. That fact, called reparameterization invariance, is a theorem in the framework's machine-checked library of formal theorems.

The geodesic length connects to probability through a second quantity, the rate action. The rate action is defined as A = −ln(sin θ_s). For angles in the allowed range, A is always positive. The framework proves that the Born weight, the probability of the outcome, equals exp(−2A), which simplifies to sin²(θ_s). That is exactly the squared amplitude of the initial state. The other outcome has probability cos²(θ_s), and the two probabilities sum to 1, as they must. So the geometry of the shortest path directly produces the familiar quantum rule that probabilities are squared amplitudes.

In Recognition Science, the framework models measurement as a forced rotation along this geodesic. The framework's library proves that the geodesic length is π/2 − θ_s, that the rate action is positive, that the Born weight equals sin²(θ_s), and that the two outcome probabilities sum to one. These are not empirical guesses; they are theorems checked by the machine. The plain-language consequence: a quantum measurement is not a mysterious collapse but a definite geometric motion, and the odds of each outcome are fixed by the length of the path the state must travel.

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

This module does not derive the Born rule from first principles; it shows that the squared-amplitude form follows from the geodesic geometry. The geodesic length is not claimed to be the only possible measure of measurement cost. No claim is made that this geometry applies to measurements with more than two outcomes.

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: