rateAction
plain-language theorem explainer
The rate action for a two-branch quantum measurement rotation is defined as the negative natural logarithm of the sine of its starting angle θ_s. Researchers deriving the Born rule from geodesic lengths in the Recognition Science framework would reference this definition when bridging path actions to probability weights. The definition directly implements equation (4.7) from the Local-Collapse paper as a one-line expression.
Claim. For a two-branch rotation with starting angle $0 < θ_s < π/2$, the rate action is $A = -ln(sin θ_s)$.
background
The module formalizes the two-branch rotation geometry from Local-Collapse §3 and Appendix A. A TwoBranchRotation structure consists of a starting angle θ_s in (0, π/2), a positive duration T, and associated bounds; the residual norm is π/2 - θ_s, the geodesic length on the Bloch sphere. Key results include the rate action A = -ln(sin θ_s) and the Born weight exp(-2A) = sin²(θ_s).
proof idea
This is a one-line definition that directly sets rateAction rot to -Real.log(Real.sin rot.θ_s), matching the formula in the module documentation.
why it matters
This definition is used by the C=2A bridge theorems in C2ABridge, including measurement_bridge_C_eq_2A which proves pathAction equals twice the rate action, and weight_equals_born which shows the weight equals the initial amplitude squared. It fills in the rate action component of the measurement bridge from Local-Collapse, enabling the derivation of Born probabilities from recognition actions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.