WickActionContinuationCert
plain-language theorem explainer
A multi-field Prop certificate that freezes, at fixed CDT ratio α > 7/12, what a full Wick continuation of the 4d three-pent hinge action must satisfy: chart agreement with the (3,2) Lorentzian simplex, branch-regular complex arccos along the open arc, continuous action on [0,1], Euclidean and Lorentzian anchors, nonzero rapidity, and a real Euclidean Schläfli derivative. Gravity/CDT workers cite it as the shape of gap-6 action-level continuation. It is a pure schema definition; inhabitation is deferred.
Claim. For fixed real $\alpha$, the certificate asserts: $\alpha > 7/12$; the three induced pentagon squared-edge charts at scale $1$ equal the standard Lorentzian $(3,2)$ chart; for every $t \in (0,1)$ the hinge-cosine path stays off the arccos cut and both slit-plane clauses for the complex-arccos log argument hold; the complex action path is continuous on $[0,1]$; at $t=1$ the cosine is the real Euclidean model cosine (and equals $-1/4$ when $\alpha=1$), and the action equals the real deficit-weighted Regge value $A(2\pi-3\arccos(\cos_E))$ ; as $t\to 0^+$ the action tends to the complex Lorentzian anchor $A(2\pi-3\theta_L)-i A(3\eta)$ with rapidity $\eta\neq 0$; and the real Euclidean endpoint action admits a derivative in $\alpha$.
background
Wave C4 R2 freezes the target for 4d causal dynamical triangulation (CDT) Wick continuation of the interior-hinge Regge action. The binding arc runs $t=0$ Lorentzian to $t=1$ Euclidean. On the three-pent object the shared hinge is the same-slice all-spacelike triangle; the three dihedral cosine paths collapse definitionally to one chart pair, so the angle sum is $3\theta(t)$ and hinge area squared is the constant real $3/16$.
Complex angle uses $\mathrm{carccos},w := -i\log(w+i\sqrt{1-w^2})$ with the repo half-power square root applied only to $1-w^2$. Branch regularity demands the cosine path off the arccos cut and both log-argument factors in the slit plane. The Lorentzian anchor is a one-sided complex limit through the cut, not a pointwise evaluation at $t=0$.
The module lands only the frozen schema plus foundation lemmas N1 (slit-plane algebra and continuity of carccos) and N2 (carccos agrees with real arccos on $(-1,1)$). It does not inhabit the terminal Prop or flip any action-level ledger Bool.
proof idea
No proof body: this is a structure-as-Prop whose fields are the certificate obligations. Each field is a named hypothesis shape (range inequality, three chart equalities, a $\forall t\in(0,1)$ branch-regularity conjunction, ContinuousOn of the action path, Euclidean cosine and action anchors, a Tendsto Lorentzian anchor, rapidity nonvanishing, and existence of a real derivative of the Euclidean endpoint action). Downstream theorems discharge individual fields (e.g. the explicit Schläfli derivative, or the no-go that continuity fails at $\alpha=1$); the structure itself only freezes the conjunction.
why it matters
This is the frozen action-level certificate for gap-6 Lorentzian Wick continuation in the SevenGaps gravity campaign. The ledger-named terminal wick_action_continuation_4d is exactly universal quantification of this certificate over $\alpha>7/12$ conjoined with the instance at $\alpha=1$ (the explicit $\mathrm{Cert},1$ kills vacuity). Status packaging records that the schema is frozen while the ledger flag stays unflipped.
Downstream, euclidSchlaefli_holds inhabits the Euclidean variation field with $S'=-3A\theta'$, and contAction_not_satisfiable_at_one is a named no-go: the continuous-action field cannot hold at $\alpha=1$. The design deliberately refuses the AND-shell of three banked branch-regular facts sold as a deficit-sum certificate, and refuses a real-only Lorentzian endpoint. In the broader RS chain this sits under gravity/Regge packaging rather than T0–T8 forcing, but it is the concrete analytic target for carrying the eight-tick causal simplex action across the Wick cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.