pentHingeCosPath_one_zero
plain-language theorem explainer
At the Lorentzian cut (t = 0) with hinge parameter α = 1, the three-pent hinge cosine path equals the model Lorentzian-endpoint cosine, namely −11/8 as a complex number. Gravity and Wick-action certificates cite this point evaluation when assembling carccos at the cut. The proof is a one-line wrapper: apply the general α-family identity with a norm_num check that 1 > 7/12.
Claim. The three-pent hinge cosine path at parameters $\alpha = 1$ and $t = 0$ equals the complex embedding of the model Lorentzian-endpoint cosine at $\alpha = 1$: $\mathrm{pentHingeCosPath}(1,0) = \mathrm{lorentzCos}(1)$ in $\mathbb{C}$. Explicitly, the right-hand side is $-(11/8)$.
background
This module closes Wave C4 items N3–N4 on Moebius confinement and Lorentzian cut-boundary values for the three-pent Wick action interior hinge. It does not inhabit the terminal, flip gap6, or touch Schläfli.
The shared path pentHingeCosPath(α,t) is the dihedral cosine split on chart pair (3,4) of the threeTwo continuation edges at structural collapse a = 1. The model Lorentzian-endpoint cosine is the real Moebius value at z = −α,
$\mathrm{lorentzCos}(\alpha) = -\frac{5+6\alpha}{2+6\alpha}$,
banked as −11/8 when α = 1. Path equality N3 identifies the hinge path at t = 0 with this real value once α lies in the causal range α > 7/12.
The parent identity pentHingeCosPath_eq_lorentzCos already proves the equality for every such α by reducing through the Moebius form and the arc chart at zero.
proof idea
One-line wrapper. Instantiate pentHingeCosPath_eq_lorentzCos at α = 1, discharging the hypothesis (7/12) < 1 by norm_num. No further algebraic work: the general Moebius reduction and real identification are inherited from that lemma.
why it matters
Feeds the certificate assembly theorem carccos_at_lorentz_cut_one, which rewrites the principal complex arccos at the cut cosine to $\pi - i,\mathrm{arcosh}(11/8)$ by substituting this point value and the banked lorentzCos_one. That is the concrete Lorentzian cut-boundary evaluation needed for the Wick-action rapidity pin and the N4 packaging path.
Within the SevenGaps gravity stack this is the α = 1 specialization of the N3 Moebius/path-equality closure: the hinge cosine lands on the real Lorentzian endpoint rather than a complex interior value. It does not resolve the still-open cut-boundary Tendsto props (carccos_tendsto_at_cut_one, lorentzAnchor_one); those remain design-authorized named interfaces. Landmark contact is local to the Wick three-pent hinge, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.