amplitudes_normalized
plain-language theorem explainer
The theorem shows that squared initial and complement amplitudes sum to one for any two-branch rotation. Physicists modeling quantum measurement via Bloch-sphere geodesics in Recognition Science cite it to confirm Born-rule normalization. The proof is a direct term-mode reduction that unfolds the amplitude definitions and applies the identity sin²θ + cos²θ = 1.
Claim. Let rot be a two-branch rotation with starting angle θ_s ∈ (0, π/2). Then sin²(θ_s) + cos²(θ_s) = 1.
background
The module formalizes two-branch quantum measurement geometry from Local-Collapse §3. A TwoBranchRotation is a structure carrying a starting angle θ_s (0 < θ_s < π/2) that sets the initial amplitude, a positive duration T, residual norm π/2 - θ_s, rate action -ln(sin θ_s), and Born weight sin²(θ_s) = |α₂|². The local setting treats the rotation as a geodesic whose length and action yield the measurement probabilities directly from the angle.
proof idea
The term proof unfolds initialAmplitudeSquared and complementAmplitudeSquared, then applies the Mathlib identity Real.sin_sq_add_cos_sq at rot.θ_s to obtain the sum equal to one.
why it matters
This normalization step secures probability conservation inside the two-branch geodesic model and directly supports the Born weight and rate-action formulas given in the module. It closes the amplitude bookkeeping required before downstream ledger and forcing constructions can assign physical masses or fluxes. No open scaffolding remains for this specific identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.