Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency

show as:
view Lean formalization →

Three pentachora glued on one interior hinge need a single CDT slice assignment on their six vertices. The module fixes hinge vertices on slice t and link vertices on t+1, then records induced causal squared lengths and the chart-cover, injectivity, and shared-face lemmas that make the complex a coherent Lorentzian 4-piece. Wick-action and gap-6 lookalike receipts import it as the kinematical scaffold for the interior-hinge Regge term.

claimFor the six vertices of a three-pentachoron interior hinge, the hinge triangle $\{0,1,2\}$ lies on time slice $t$ and the link vertices $\{3,4,5\}$ lie on slice $t+1$. Three pentachoron vertex charts cover the complex injectively, induce matching causal squared edge lengths on shared faces, and agree on the common hinge.

background

The QG Seven-Gaps Lorentzian lane lifts 3D causal-simplex machinery to 4D CDT-style 4-simplices (pentachora). Upstream CausalSimplex4D supplies the causal 4-simplex classes and the kinematical Wick-rotation setting in $D=4$. Upstream ThreePentInteriorHingeWitness supplies the positive half of the interior-hinge gate: the minimal complex whose hinge link is a cycle (three pents are necessary by the two-pent counting lemma).

This module sits between those two. It fixes slice membership for the six vertices of that minimal complex: hinge ${0,1,2}$ on slice $t$ (false), link ${3,4,5}$ on $t+1$ (true). From that assignment it builds causal squared lengths, three pent charts, and the consistency facts (cover, injectivity, slice match, shared-face edge agreement) needed before any glued-pent expression may be treated as a Regge action term.

proof idea

Definition-heavy consistency module, not a single deep theorem. It introduces slice membership on the six vertices, a causal squared-length function on edges (with symmetry), and three explicit pentachoron vertex charts. Cover and injectivity of the charts are proved by finite case analysis on the vertex labels. Slice-matching and induced-edge lemmas reduce to rewriting the shared faces against the common hinge assignment. Shared-face consistency and the induced-pent equality are algebraic identities on those charts, discharging the requirement that the three-pent complex carries one coherent causal metric skeleton.

why it matters in Recognition Science

Panel P1-remainder and Wave C4 treat the three-pent interior hinge as the minimal place where a cyclic hinge link exists, so glued-pent expressions may be called Regge action. Without causal consistency of that complex, the Wick continuation and certificate assembly have no kinematical carrier.

Downstream, WickActionInteriorHinge freezes the wick_action_continuation_4d schema and the carccos lift (N1+N2) on this hinge; WickActionCertAssembly compares the pointwise carccos value against the N4 one-sided cut; Gap6LookalikeReceipt banks lookalike-falsify theorems against decoy residual gap-6 claims. The module is the shared causal scaffold those receipts import. It does not itself close the Wick action or the alpha-band constants; it only makes the three-pent Lorentzian piece well-defined.

scope and limits

used by (3)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (23)