TwoBranchRotation
plain-language theorem explainer
TwoBranchRotation packages 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 theorists cite it when building recognition paths that recover Born weights from rate actions. The declaration is a bare structure with four fields and no computational or proof content.
Claim. A two-branch rotation is a pair of real numbers θ_s, T satisfying 0 < θ_s < π/2 and 0 < T, where θ_s sets the initial amplitude and the residual action equals π/2 - θ_s.
background
The module formalizes two-branch rotation geometry from Local-Collapse §3 and Appendix A. It records residual norm ||R|| = π/2 - θ_s as geodesic length, rate action A = -ln(sin θ_s), and Born weight exp(-2A) = sin²(θ_s) = |α₂|². The structure supplies the input data for pathFromRotation, which defines a RecognitionPath with duration π/2 - θ_s and rate given by the recognition profile shifted by θ_s. Upstream module imports include LedgerFactorization and PhiForcingDerived for J-cost calibration, though the local setting centers on measurement geometry rather than those structures.
proof idea
This is a structure definition with zero proof lines. It declares four fields (θ_s with bounds, T with positivity) and serves as a data carrier; downstream theorems unfold it directly via pattern matching on the fields.
why it matters
The structure supplies rotation data to the C=2A bridge theorems measurement_bridge_C_eq_2A and weight_equals_born, which equate path action to twice the rate action and show weights recover Born probabilities. It also feeds born_rule_from_C and amplitude_modulus_bridge. The definition operationalizes the two-branch geodesic that converts recognition actions into quantum measurement weights, linking the Recognition Composition Law to the Born rule in the Measurement domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.