Measurement Two Branch Geodesic Born Weight From Rate

The Born weight identity

In quantum mechanics, the Born rule is the recipe that turns a wavefunction into a probability: the chance of seeing a particular outcome equals the squared magnitude of the corresponding amplitude. For a two-outcome measurement on a qubit, if the initial amplitude for outcome two is α₂, the Born rule says the probability is |α₂|². The Recognition Science declaration born_weight_from_rate shows that this same probability can be computed from a geometric quantity called the rate action, which measures how fast a rotation on the Bloch sphere proceeds.

The setup is a two-branch rotation: a starting angle θ_s between 0 and π/2, and a duration T. The rotation moves the state from θ_s to π/2, the equator of the Bloch sphere. The residual action is the geodesic length of this rotation, π/2 − θ_s. The rate action A is defined as −ln(sin θ_s), a positive number that grows as the starting angle shrinks. The theorem states that exp(−2A) = sin²(θ_s) = |α₂|². In words: the Born weight, the probability of the outcome, equals the exponential of minus twice the rate action, which in turn equals the squared sine of the starting angle.

The declaration also proves that the two amplitudes sum to one: sin²(θ_s) + cos²(θ_s) = 1, which is the normalization condition for a valid probability distribution. It further shows that the residual action is invariant under reparameterization of time, meaning the geodesic length does not depend on how fast the rotation is traversed. These results are proved in the framework's machine-checked library of formal theorems, meaning the algebraic steps are verified by a computer.

What the declaration does not claim is that this geometric derivation replaces the physical Born rule or explains why measurement outcomes occur. The theorem is a mathematical identity within a specific geometric model of a two-branch measurement. It does not address the measurement problem, the collapse of the wavefunction, or the physical mechanism by which a definite outcome emerges. It also does not generalize to measurements with more than two outcomes or to continuous observables, which would require additional structure not present in this declaration.

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

/-- Rate action A = -ln(sin θ_s) from eq (4.7) of Local-Collapse -/
noncomputable def rateAction (rot : TwoBranchRotation) : ℝ :=
  - Real.log (Real.sin rot.θ_s)

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

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

What this page does not claim

The declaration does not explain the physical mechanism of wavefunction collapse. It does not generalize to measurements with more than two outcomes. It does not derive the Born rule from first principles independent of the geometric model.

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: