Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit

show as:
view Lean formalization →

One-sided cut-boundary limits for the complex arccos of the pentagon-hinge cosine path at coupling α = 1, written so the log-argument limit matches the sum of the L2 and L3 pieces. Gravity and QG workers in the Seven-Gaps campaign cite it as the N4 cut-limit core at the physical point. The argument is a six-lemma route: slit-plane membership for 57/64, square-root and path tendsto facts, and eventual real/imaginary sign control feeding the complex-arccos log-argument identity.

claimAt $\alpha = 1$, the module establishes the one-sided neighborhood limits for the cut value of complex inverse cosine along the pentagon-hinge path: $\sqrt{z^2-1}$ and the associated log-arguments tend so the boundary value equals $\pi + i\,\mathrm{arcosh}(11/8)$, matching the sum of the L2 and L3 limit contributions. Supporting facts include $57/64$ in the slit plane and $\sqrt{57}/8 = \sqrt{(11/8)^2-1}$.

background

Recognition Science gravity packages Wick rotation of the (4,1) causal 4-simplex action as a complex-first continuation across triangular hinges. Upstream, the interior-hinge module freezes the schema for the four-dimensional Wick-action continuation certificate and lifts real arccos to complex arccos on the slit plane (foundation lemmas N1–N2: slit-plane membership and continuity, plus real-agreement). The confinement module closes Moebius collapse and $\mathrm{Im}<0$ confinement on the causal $\alpha$-range (N3), leaving cut-boundary Tendsto as named N4 obligations after Mathlib one-sided log/csqrt filter limits resisted a direct attack.

This module is the $\alpha=1$ N4 cut core. The pentagon-hinge cosine path is the model path near the Lorentzian cut; the target boundary value is $\pi+i,\mathrm{arcosh}(11/8)$. Algebraically $(11/8)^2-1=57/64$, so the companion constant is $\sqrt{57}/8$. Mathlib complex log, arg, square root, and arcosh supply the analytic toolkit; the all-hinges upstream module extends split-form branch regularity from one traced hinge to all ten triangles of the fourOne type.

proof idea

Not one theorem: a coordinated six-lemma route at $\alpha=1$. Place $57/64$ in the slit plane and identify $\sqrt{57}/8$. Prove tendsto of the pentagon-hinge cosine path toward 1 and of $\mathrm{csqrt}(z^2-1)$ along that approach. Obtain eventual control in a punctured neighborhood of the cut: real part of the path negative, imaginary parts of the path and of $1-z^2$ negative, positive real part of the square root when the imaginary part is negative, and equality of the complex-arccos expression with the explicit log-argument form. Those eventualities assemble the one-sided cut limit written to match the sum of the L2 and L3 pieces.

why it matters in Recognition Science

Closes the $\alpha=1$ cut-limit spine of Wave C4 N4 in the Seven-Gaps gravity campaign (design freeze D-gap6-r1). Downstream certificate assembly at $\alpha=1$ compares the pointwise complex-arccos value of the pentagon-hinge path at the physical point with this N4 one-sided cut limit $\pi+i,\mathrm{arcosh}(11/8)$, as the first assembly obligation. The audit module checks that headline theorems print inside the standard axiom set. The parameterized family module generalizes the same six-lemma route from $\alpha=1$ to the full causal range $\alpha>7/12$ (pointwise only; no uniform-in-$\alpha$ bound, since the Lorentz factor tends to 1 as $\alpha\to\infty$). Together they feed the partial receipt for Wick-action continuation across the fourOne hinges.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (33)