initialAmplitudeSquared
initialAmplitudeSquared assigns sin²(θ_s) as the squared modulus of the initial amplitude for any two-branch rotation. Measurement theorists deriving Born probabilities from geodesic actions or C=2A bridges cite it to equate rotation angle directly to probability weight. The definition is a direct one-line extraction from the θ_s field of the input structure.
claimFor a two-branch rotation with starting angle θ_s ∈ (0, π/2), the squared modulus of the initial amplitude is defined by |α₂|² := sin²(θ_s).
background
The TwoBranchGeodesic module encodes the two-branch quantum measurement geometry from Local-Collapse §3. A TwoBranchRotation is the structure carrying starting angle θ_s (with 0 < θ_s < π/2), positive duration T, and the residual geodesic length π/2 - θ_s. The rate action A = -ln(sin θ_s) then yields Born weight exp(-2A) = sin²(θ_s). Upstream amplitude definitions from S-matrix unitarity and double-slit path phases supply the complex-amplitude context that this real-valued extraction specializes.
proof idea
One-line definition that applies the sine-squared operation directly to the θ_s component of the supplied TwoBranchRotation structure.
why it matters in Recognition Science
This definition supplies the explicit geometric expression for |α₂|² that is invoked in born_rule_from_C to obtain the two-outcome measurement and in weight_equals_born to equate path weight with Born probability. It thereby closes the C=2A bridge inside the Recognition measurement layer and aligns with the eight-tick octave and phi-ladder mass formula. It touches the open question of whether all probability weights descend from the T5 J-uniqueness and RCL without extra postulates.
scope and limits
- Does not compute amplitudes for multi-branch or continuous spectra.
- Does not incorporate dynamical time evolution beyond the fixed T parameter.
- Does not prove normalization; that is supplied separately by amplitudes_normalized.
- Does not retain complex phase information, only the squared modulus.
formal statement (Lean)
72noncomputable def initialAmplitudeSquared (rot : TwoBranchRotation) : ℝ :=
proof body
Definition body.
73 (Real.sin rot.θ_s) ^ 2
74
75/-- Complement amplitude |α₁|² = cos²(θ_s) -/