residualAction
plain-language theorem explainer
The residualAction definition assigns to each two-branch rotation the value π/2 minus its starting angle θ_s, which equals the geodesic length on the Bloch sphere. Researchers formalizing quantum measurement in the Recognition Science setting cite this when deriving residual norms or checking reparameterization invariance. It is realized as a direct subtraction in the definition body.
Claim. For a two-branch rotation with starting angle $θ_s$ satisfying $0 < θ_s < π/2$, the residual action is $S = π/2 - θ_s$, the geodesic length on the Bloch sphere.
background
This definition sits in the Two-Branch Quantum Measurement Geodesic module, which formalizes the two-branch rotation geometry from Local-Collapse §3 and Appendix A. The TwoBranchRotation structure packages a starting angle θ_s (with bounds 0 < θ_s < π/2), a positive duration T, and the associated positivity proofs. The module documentation identifies the residual action with the geodesic length on the Bloch sphere and lists it among the key results alongside the rate action and Born weights.
proof idea
The definition is a one-line wrapper that subtracts the starting angle θ_s from π/2.
why it matters
This supplies the concrete value of the residual action that feeds residual_action_invariant (which records reparameterization invariance via reflexivity) and residualNorm (which re-exports the same quantity). It realizes the first key result stated in the module documentation and connects the two-branch geometry to the measurement process in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.