residual_action_invariant
plain-language theorem explainer
Residual action for any two-branch rotation equals π/2 minus its starting angle θ_s. Physicists deriving Born weights from Bloch-sphere geodesics cite the identity to confirm reparameterization invariance of the residual norm. The proof is a one-line reflexivity that matches the definition of residualAction exactly.
Claim. For a two-branch rotation rot with starting angle θ_s (where 0 < θ_s < π/2), the residual action S(rot) satisfies S(rot) = π/2 - θ_s.
background
The module formalizes two-branch quantum measurement geometry from Local-Collapse §3. A TwoBranchRotation is the structure carrying starting angle θ_s (0 < θ_s < π/2) and positive duration T; residualAction is the noncomputable definition that returns exactly π/2 - θ_s, interpreted as geodesic length on the Bloch sphere. Upstream Measurement structures supply the protocol and uncertainty context in which the rotation occurs.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity directly to the definition of residualAction.
why it matters
The declaration confirms the reparameterization invariance stated in the module doc-comment and anchors the key result ||R|| = π/2 - θ_s. It supports the downstream derivation of rate action A = -ln(sin θ_s) and Born weight sin²(θ_s) = |α₂|². Within Recognition Science it fixes the measurement geometry inside the two-branch model without invoking the phi-ladder or forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.