Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete

show as:
view Lean formalization →

Module B3 closes hinge-data Wick continuation for every triangular hinge of both causal 4-simplex types at the physical point. For each unordered opposite vertex pair and both orientations, the split-form complex-first path is branch-regular on the open arc and continuous on the closed interval ending at the Euclidean cosine -1/4. Gravity and discrete-QG workers cite it as the finished data layer under C11. It aggregates the (4,1) and (3,2) all-hinge certificates already proved upstream.

claimAt $a=1$, $\alpha=1$, for every triangular hinge (every unordered opposite vertex pair $\{p,q\}$, both orientations) of both causal 4-simplex types $(4,1)$ and $(3,2)$, the split-form complex-first Wick continuation is branch-regular on the open arc interior $(0,1)$ and extends continuously on the closed interval $[0,1]$ to the Euclidean regular-4-simplex cosine $-1/4$. Scope is hinge data only (dihedral cosines and areas-squared).

background

The QG Seven-Gaps campaign treats 4D Lorentzian Regge calculus via a complex-first Wick path. Lane C11 (WickActionComplexFirst) fixes the split-form formalization and the canonical upper-half-plane arc, with hour-0 numeric gate receipts for branch crossing. A hinge is a triangular face of a 4-simplex together with its opposite edge; the data of interest are the dihedral cosine and the area-squared along that hinge.

Lane B1 (WickFourOneAllHinges) lifts the single traced hinge of the $(4,1)$ causal 4-simplex to all ten triangular hinges at the physical point. Lane B2 (WickThreeTwoHinges) does the same for all ten hinges of the $(3,2)$ type, and records the remaining product-form kill certificates from the executed trace. This module is the B3 headline that packages both all-hinge results into one complete hinge-data continuation statement.

Action-level continuation remains deliberately out of scope: the C12 three-pent interior-hinge complex is still required before any full action path can be certified.

proof idea

Aggregator module over the two all-hinge lanes. It imports the complex-first arc and split-form infrastructure from WickActionComplexFirst, then invokes the exhaustive hinge certificates of WickFourOneAllHinges (ten hinges of type $(4,1)$) and WickThreeTwoHinges (ten hinges of type $(3,2)$, plus product-form kills). The headline theorem states branch-regularity on the open arc and continuous closed-interval continuation to $-1/4$ for every hinge of both types. Sibling flags record closed-form area-squared identities, memorialized product-form kills, and the explicit open status of the action-level path.

why it matters in Recognition Science

Closes the hinge-DATA half of the Wick-continuation finishing charter (B3) under the C11 complex-first mandate. Downstream gravity and full-theory ledger work can treat every single-simplex triangular hinge of both causal 4-simplex types as having a certified complex-first path to the Euclidean regular value, without reopening branch or boundary questions at the data layer.

The module does not touch FullTheoryLedger flags and does not claim action-level continuation; that stays open pending the C12 three-pent interior-hinge complex. In the broader Recognition gravity stack this is the discrete-geometry prerequisite that lets later curvature and deficit arguments sit on a completed Wick data layer rather than on a single traced hinge.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (4)