wick_hinge_data_continuation_complete
plain-language theorem explainer
For every triangular hinge of both causal 4-simplex types (4+1 and 3+2), at the physical point a=α=1, the split-form complex-first Wick path of the dihedral cosine is branch-regular on (0,1), continuous on [0,1], and ends at the Euclidean value −1/4. Gravity and discrete-QG workers cite it as the B3 completeness certificate for hinge-data continuation. The proof is a thin packaging of the per-type B1 and B2 hinge lemmas.
Claim. For every pair of distinct vertices $p,q\in\{0,1,2,3,4\}$, both of the following hold at $a=1$, $\alpha=1$: (i) the $4{+}1$ continuation edge map is branch-regular on $(0,1)$, the $4{+}1$ cosine path is continuous on $[0,1]$, and its value at $1$ is $-(1/4)$; (ii) the same three statements for the $3{+}2$ continuation edge map and cosine path.
background
Lane B3 of the QG Seven-Gaps campaign packages hinge-data Wick continuation over both causal 4-simplex types. A causal 4-simplex is a 5-vertex simplex with either signature class 4+1 (one timelike edge class) or 3+2. Each unordered opposite vertex pair ${p,q}$ labels a triangular hinge (the complementary triple). The objects continued are the dihedral cosines along the canonical upper-half-plane arc at the physical point $a=1$, $\alpha=1$.
Branch regularity means the complex-first split-form edge continuation stays off the branch cut on the open arc interior. Continuity is required on the closed interval so the Euclidean endpoint is attained. That endpoint is the regular Euclidean 4-simplex cosine $-(1/4)$.
Upstream, B1 (WickFourOneAllHinges) supplies the full 4+1 hinge certificates, and B2 (WickThreeTwoHinges) supplies the 3+2 certificates. This module only conjoins them. Honest scope from the module doc: this is hinge data of a single simplex per type, not an action-level continuation of deficit angles over a multi-pent complex.
proof idea
Term-mode packaging after intro p q hpq. Destructure wick_boundary_continuation_fourOne_allHinges p q hpq for the 4+1 closed-interval continuity and Euclidean endpoint. Destructure wick_continuation_threeTwo_hinges p q hpq for the full 3+2 triple (branch regularity, continuity, endpoint). Pair those with branchRegular_fourOne_allHinges p q hpq for the missing 4+1 branch-regularity leg, and assemble the two conjuncts. No new analysis is performed here.
why it matters
Closes the B3 headline of the finishing charter: cosine continuation is complete for all twenty hinges and both causal types. Downstream, action_level_still_open records by rfl that the kinematical status flag action_level_continuation_open remains true; this module deliberately does not touch FullTheoryLedger.
In the Recognition gravity stack this is the data-layer prerequisite before any continued Regge action can be stated. The action-level step needs a genuine three-or-more-pent interior-hinge complex (C12 lane) and stays open. Framework contact is discrete causal geometry and Wick rotation of hinge observables, not the T0–T8 forcing chain or the mass ladder.
Sibling theorems in the same module handle areas-squared closed forms and product-form kill certificates; together they finish hinge-data continuation while keeping the action gap explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.