rate_action_pos
plain-language theorem explainer
The residual rate action A(θ_s) is strictly positive for geodesic separation angles whose sine lies strictly between 0 and 1. Workers deriving the Born rule from recognition costs cite this to guarantee that collapse rates remain positive for non-orthogonal states. The argument is a one-line wrapper that unfolds the definition A = −ln(sin θ_s) and invokes the standard negativity of the logarithm on (0,1).
Claim. If $0 < sin θ_s < 1$, then the residual rate action satisfies $A(θ_s) > 0$, where $A(θ_s) := -ln(sin θ_s)$.
background
In the coherence-collapse setting the recognition action C along a path γ is the integral of J-cost, while the residual rate action A is extracted from the geodesic separation angle θ_s. The module establishes that C equals twice A for any such rotation, yielding Born weights as exp(−C_I) normalized over the sum. Upstream, J-cost is the derived cost of a multiplicative recognizer on positive ratios, and the identity event (state = 1) has zero cost by the non-contradiction property of the comparison operator.
proof idea
The proof is a one-line wrapper. It unfolds the definition of rate_action, rewrites the goal via the equivalence 0 < −x ↔ x < 0, and applies the standard lemma that the real logarithm is strictly negative on the open interval (0,1).
why it matters
This result secures the sign of the residual action that drives the central C = 2A identity, which produces the Born rule from recognition costs. It sits inside the gravity-coherence bridge that links quantum measurement to gravitational collapse via the recognition composition law and the eight-tick octave. No open questions are directly touched; the positivity is unconditional once the sine bounds are supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.