Measurement Two Branch Geodesic Amplitudes Normalized

The two-branch amplitude rule

In the standard quantum-mechanical description of a measurement with two possible outcomes, the probabilities of the two outcomes must add up to exactly 1. If the state of the system is described by two complex numbers, often called amplitudes, then the squared magnitudes of those amplitudes, |α₁|² and |α₂|², are the probabilities. The rule that |α₁|² + |α₂|² = 1 is called normalization, and it is a basic consistency requirement: the particle must be found in one of the two outcomes.

This normalization rule is not just an axiom; it can be derived from a geometric picture. In the framework of Recognition Science, a framework that models physical structure from a discrete record of events, a two-branch measurement is represented as a rotation on the surface of a sphere, the Bloch sphere. The measurement starts at an angle θ_s and rotates to the north pole, an angle of π/2. The length of this rotation path, called the residual action, is simply π/2 - θ_s. The probability of the second outcome is then defined as the square of the sine of the starting angle, sin²(θ_s), and the probability of the first outcome is the square of the cosine, cos²(θ_s).

In the machine-checked library of formal theorems, the declaration amplitudes_normalized proves that these two probabilities, sin²(θ_s) and cos²(θ_s), sum to 1. The proof is a direct application of the standard trigonometric identity sin²(x) + cos²(x) = 1. This is a theorem in the library, meaning it is a formal, verified statement. It confirms that the geometric construction is consistent with the fundamental probabilistic rule of quantum mechanics.

What this theorem does not do is explain why a measurement should be represented by a rotation on a sphere, nor does it derive the starting angle θ_s from any deeper principle. The choice of the rotation model is a definitional choice, not a consequence of the theorem. The theorem takes the geometric setup as given and proves the normalization property that follows from it. The physical bridge from a discrete ledger of events to the continuous rotation geometry remains an open target within the framework.

The practical consequence is that the geometric model of measurement is internally consistent with the probabilistic core of quantum theory. Any further development of this model, such as computing transition rates or entropies, can rely on the fact that the two-branch amplitudes are properly normalized, so that the total probability is always 1.

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

/-- 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 theorem does not derive the rotation model itself from the ledger. This theorem does not determine the value of the starting angle θ_s.

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: