pentHingeCosPath_eq_lorentzCos
plain-language theorem explainer
For causal hinge parameters α > 7/12, the three-pent cosine path at the Lorentzian endpoint t = 0 equals the model Lorentzian cosine of α, embedded ℝ → ℂ. Gravity and Wick-rotation workers cite it to pin the cut-boundary value of the Moebius-collapsed path. The proof rewrites the path as a Moebius transform of arcZ, evaluates arcZ at 0, and matches the resulting real rational to lorentzCos by elementary algebra and casting.
Claim. Let $\alpha \in \mathbb{R}$ with $\alpha > 7/12$. Then the shared three-pent hinge cosine path at Lorentzian endpoint parameter $t = 0$ equals the complex embedding of the model Lorentzian-endpoint cosine: $c_{\mathrm{path}}(\alpha,0) = \bigl(-\frac{5+6\alpha}{2+6\alpha}\bigr)^{\mathbb{C}}$.
background
This module closes Wave C4 items N3–N4 on Moebius confinement and Lorentzian cut-boundary values for the interior hinge, without inhabiting the terminal, flipping gap6, or touching Schläfli.
The shared path pentHingeCosPath α t is the dihedral cosine split on chart pair (3,4) of the three-two continuation edges at structural radius a = 1. Upstream, that path collapses to a Moebius transform of the complex arc arcZ 1 α t whenever α > 7/12: $(5 - 6 z)/(6 z - 2)$ with $z = \mathrm{arcZ}$. At the Lorentzian endpoint t = 0 one has $\mathrm{arcZ}(a,\alpha,0) = -\alpha a^2$ (here a = 1), so the argument is simply $-\alpha$.
The model Lorentzian-endpoint cosine is the real Moebius value at $z = -\alpha$: $\mathrm{lorentzCos},\alpha = -\frac{5+6\alpha}{2+6\alpha}$. At α = 1 this recovers the banked constant −11/8. The present theorem identifies the path at t = 0 with that real model value inside ℂ.
proof idea
Rewrite the path by the Moebius collapse pentHingeCosPath_eq_moebius (valid under α > 7/12) and substitute arcZ_zero, so the argument becomes $-\alpha$ and the path is the complex quotient $(5 - 6(-\alpha))/(6(-\alpha) - 2)$.
A short real calculation shows that quotient equals lorentzCos α: expand $5 - 6(-\alpha) = 5 + 6\alpha$ and $6(-\alpha) - 2 = -(2 + 6\alpha)$, then cancel the sign via div_neg against the defining formula of lorentzCos.
Finally norm_cast moves the real division under the ℝ → ℂ embedding (after simplifying $a^2 = 1$), and rewrite finishes the equality in ℂ.
why it matters
N3 of the gap6 design asks for Moebius collapse and MODEL path equality on the causal α-family. This theorem supplies the Lorentzian endpoint of that equality: the path at t = 0 is exactly the model Lorentzian cosine, not merely some complex number near it.
Its sole recorded consumer is pentHingeCosPath_one_zero, the α = 1 specialization that pins the banked value −11/8 at the physical hinge. Together with the Euclidean-endpoint sibling and the Im < 0 confinement lemmas in the same module, it closes the cut-boundary value side of N3 while N4’s one-sided Tendsto packaging remains the open residual.
In the broader Recognition gravity stack this is local Wick-action bookkeeping on the three-pent complex, not a forcing-chain (T0–T8) step; it feeds the hinge cosine that later enters deficit-angle and rapidity certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.