residualNorm
plain-language theorem explainer
residualNorm supplies the residual norm for a two-branch rotation, obtained by delegating to residualAction. A physicist modeling quantum measurement geodesics on the Bloch sphere cites it to extract the integrated defect length from starting angle θ_s to π/2. The definition is a one-line wrapper that applies residualAction directly to the rotation structure.
Claim. Let rot be a two-branch rotation with starting angle θ_s satisfying 0 < θ_s < π/2 and duration T > 0. The residual norm is defined by ||R|| := residual action of rot, which equals the geodesic length π/2 - θ_s.
background
The module formalizes two-branch quantum measurement geometry from Local-Collapse §3 and Appendix A. A TwoBranchRotation is the structure containing starting angle θ_s in (0, π/2) and positive duration T. Residual norm is the geodesic length on the Bloch sphere. Upstream results supply ledger factorization for J-cost calibration and phi-forcing structures that fix the underlying action scale.
proof idea
This is a one-line wrapper that applies residualAction to the input rotation.
why it matters
The definition supplies the residual norm used to obtain rate action A = -ln(sin θ_s) and Born weight sin²(θ_s). It fills the measurement-geometry step in the Local-Collapse framework and connects to the eight-tick octave through spectral emergence and primitive distinction. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.