TwoBranchRotation
plain-language theorem explainer
TwoBranchRotation encodes a starting angle θ_s in (0, π/2) and positive duration T to represent a geodesic rotation from θ_s to π/2 on the Bloch sphere. Measurement formalisms cite the record to derive rate actions and equate path weights with amplitude squares. The declaration is a direct structure definition whose four fields enforce the angle bounds, time positivity, and residual length π/2 - θ_s.
Claim. A two-branch rotation consists of a real starting angle θ_s satisfying 0 < θ_s < π/2 together with a positive real duration T, such that the residual geodesic length on the Bloch sphere equals π/2 - θ_s.
background
The module formalizes two-branch quantum measurement geometry from Local-Collapse §3 and Appendix A. Residual norm is defined as π/2 - θ_s (geodesic length), rate action A as -ln(sin θ_s), and Born weight as exp(-2A) = sin²(θ_s) = |α₂|². Upstream structures supply J-cost calibration via ledger factorization, phi-tiers for physical quantities, spectral emergence of gauge content and generations, and fundamental periods T.
proof idea
This is a structure definition with no proof body. The four fields directly record θ_s, its bounds, T, and T positivity; no lemmas or tactics are applied.
why it matters
The structure supplies rotation data to the C=2A bridge theorems and Born-rule derivations. It implements the geodesic length and rate action that equate path weights with amplitude squares, closing the recognition-action link to quantum probabilities. It sits in the measurement sector where T5 J-uniqueness and the phi-ladder underpin the action functionals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.