TwoBranchRotation
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical values for θ_s or T.
- Does not prove the Born rule or normalization.
- Does not extend to multi-branch or continuous measurements.
- Does not assign phi-ladder rungs or incorporate G or alpha constants.
Lean usage
theorem weight_equals_born (rot : TwoBranchRotation) : pathWeight (pathFromRotation rot) = initialAmplitudeSquared rot := by exact Measurement.C2ABridge.weight_equals_born rotformal statement (Lean)
22structure TwoBranchRotation where
23 θ_s : ℝ -- starting angle (determines initial amplitude)
24 θ_s_bounds : 0 < θ_s ∧ θ_s < π/2
25 T : ℝ -- duration of rotation
26 T_pos : 0 < T
27
28/-- Residual action S = π/2 - θ_s (geodesic length on Bloch sphere) -/
used by (16)
-
born_rule_from_C -
amplitude_modulus_bridge -
measurement_bridge_C_eq_2A -
pathFromRotation -
weight_bridge -
weight_equals_born -
C_equals_2A -
amplitudes_normalized -
born_weight_from_rate -
complementAmplitudeSquared -
initialAmplitudeSquared -
rateAction -
rateAction_pos -
residualAction -
residual_action_invariant -
residualNorm