rapidityPinned_one
plain-language theorem explainer
At the physical coupling α = 1 the Lorentz rapidity is nonzero. Certificate authors for the Wick-action continuation cite this as the rapidityPinned field. The proof evaluates the Lorentzian cosine to −11/8, takes absolute value, and invokes positivity of arcosh on (1, ∞).
Claim. At the physical coupling $\alpha = 1$, the Lorentz rapidity $\operatorname{arcosh}\lvert C_L(1)\rvert$ is nonzero, where $C_L$ denotes the Lorentzian cosine of the interior hinge.
background
This module closes Wave C4 items N3 and N4 on Moebius confinement and the Lorentzian cut-boundary value for the Wick interior hinge (fable design D-gap6-r1). N3 handles the α-family on the causal range; N4 owns cut-boundary limits and the rapidity pin. The module does not inhabit the terminal certificate, flip gap6, or touch Schläfli.
The Lorentz rapidity is defined as $\operatorname{arcosh}\lvert C_L(\alpha)\rvert$, where $C_L$ is the Lorentzian cosine of the boost angle on the interior hinge. Its nonzeroness is exactly the rapidityPinned certificate field. Upstream, $C_L(1) = -11/8$ is already proved by direct unfolding and numeric evaluation.
Real part of the Lorentzian boost angle is frozen at $\pi$ (principal value when $\cos \le -1$); N4 owns the one-sided limit identification separately from this pin.
proof idea
Term-mode proof. Unfold the rapidity definition to $\operatorname{arcosh}\lvert C_L(1)\rvert$. Rewrite with the closed evaluation $C_L(1) = -11/8$, then simplify absolute value via $\lvert -x\rvert = \lvert x\rvert$ and nonnegativity of $11/8$. The goal is $\operatorname{arcosh}(11/8) \ne 0$. Apply Mathlib's Real.arcosh_pos at the numeric witness $1 < 11/8$, then take .ne'.
why it matters
Closes the N4 decoy/pin item rapidityPinned_one authorized by the gap6 design session: a concrete nonzero rapidity at the physical coupling, banked while the sharper cut-boundary Tendsto stays open. Downstream it feeds wickActionContinuationCertV2_one, the repaired V2 certificate at α = 1 (causal range, chart agreement, branch-regular sum, interior continuity), which is a partial receipt and does not yet inhabit the full 4d Wick-action continuation.
In the Recognition gravity stack this is local scaffolding for the Lorentzian side of the interior-hinge Wick path, not a T0–T8 forcing step. It keeps the rapidity certificate field honest so later assembly can package R5 toward the sharper-blocker path if the one-sided log/csqrt limit remains unresolved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.