Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFamilyThreshold

show as:
view Lean formalization →

Tracks Wick Euclidean-admission thresholds for the two CDT causal 4-simplex types, (4,1) and (3,2). Labels which causal class is under study via a thin enum wrapper, then compares the two continuation thresholds. Gravity and CDT workers cite it when separating kinematical Wick windows by simplex type. The argument is definitional indexing plus elementary comparisons of the assembled alpha-minima.

claimFor each CDT causal 4-simplex class $C\in\{(4,1),(3,2)\}$, define the Wick continuation threshold $\alpha_{\min}(C)$ as the Euclidean-admission cutoff of the associated Lorentzian edge data. The module records $\alpha_{\min}(4,1)$, $\alpha_{\min}(3,2)$, proves they differ, and proves $\alpha_{\min}(4,1)<\alpha_{\min}(3,2)$.

background

This sits in the QG Seven-Gaps Lorentzian-sector lane (Phase 3a), the 4D lift of the kernel-checked 3D causal-simplex Wick machinery. Causal dynamical triangulations (CDT) classify 4-simplices by how many vertices lie on each successive spatial slice; the two relevant causal types are the (4,1) and (3,2) classes.

Upstream CausalSimplex4D supplies the causal 4-simplex classes and the kinematical Wick rotation in $D=4$. Geometric content (squared Lorentzian edge lengths, the 4D Cayley-Menger data) lives there, not in the label type of this module. Upstream WickActionCertAssembly assembles certificates at $\alpha=1$ and compares pointwise arccos hinge data against the one-sided cut limit $\pi+i,\mathrm{arcosh}(11/8)$.

The module's own index type is deliberately thin: a one-field wrapper on a two-constructor enum. It names which causal type is tracked; it carries no simplices, incidence, or gluing.

proof idea

Definition layer first: an enum of the two causal Wick complexes, constructors for the (4,1) and (3,2) inhabitants, and a predicate for Euclidean admissibility under Wick continuation. Thresholds are obtained by reading off the assembled $\alpha_{\min}$ for each class (equality lemmas identify the named constants with that minimum).

Comparison layer: separate lemmas give the numerical/structural values for the two thresholds, then a difference lemma and a strict inequality $\alpha_{\min}(4,1)<\alpha_{\min}(3,2)$. Proofs are short algebraic or norm_num/linarith style comparisons against the imported certificate assembly, not a reconstruction of the simplicial geometry.

why it matters in Recognition Science

In the Seven-Gaps gravity campaign, Wick admission must be stated per causal 4-simplex class before any global Euclidean sector claim. This module isolates that family-level threshold comparison so later certificate and action work can cite distinct windows for (4,1) versus (3,2) rather than a single undifferentiated cutoff.

It consumes the 4D causal-simplex and Wick-certificate assembly imports and exposes named thresholds, their equality to $\alpha_{\min}$, and the strict ordering between classes. No downstream edges are recorded yet in the mirror graph; the natural consumers are higher Wick-action and gap-closure receipts that need class-indexed admissibility. Landmark contact is the $D=4$ Lorentzian lift (spatial $D=3$ plus time) inside the CDT causal calculus, not the T5-T8 forcing chain directly.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (25)