complementAmplitudeSquared
plain-language theorem explainer
The definition supplies the complement amplitude squared as cos²(θ_s) for any two-branch rotation structure. Quantum measurement theorists deriving probabilities from Bloch sphere geodesics would cite it to connect rotation angle to |α₁|². It is realized as a direct one-line extraction of the squared cosine from the rotation's starting angle field.
Claim. For a two-branch rotation with starting angle θ_s satisfying 0 < θ_s < π/2, the complement amplitude squared equals cos²(θ_s).
background
The module formalizes two-branch quantum measurement rotations drawn from Local-Collapse §3. A TwoBranchRotation structure packages a starting angle θ_s in (0, π/2), a positive duration T, and the geometric relation that maps θ_s to initial amplitude sin θ_s and complement amplitude cos θ_s. The local setting treats the residual norm as π/2 - θ_s (geodesic length) and the rate action as -ln(sin θ_s), with the Born weight then given by sin²(θ_s). The upstream TwoBranchRotation definition supplies the angle parameter that this extraction directly consumes.
proof idea
The definition is a one-line wrapper that squares the cosine of the rotation's starting angle θ_s.
why it matters
This definition supplies the complement amplitude used by amplitudes_normalized to prove normalization and by born_rule_from_C to establish that probabilities match amplitude squares. It thereby closes the geometric link between two-branch rotation and the Born rule inside the Recognition Science measurement model. The construction aligns with the framework's emphasis on deriving quantum probabilities from geodesic actions without additional postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.