IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFamilyThreshold
Module that indexes the two CDT causal 4-simplex classes and records their Wick Euclidean-admission thresholds. Gravity and CDT workers cite it when comparing the (4,1) and (3,2) continuation cutoffs. The content is definitional plus elementary comparisons: a two-value label, threshold extraction from the causal metric data, and proofs that the two thresholds differ and are ordered.
claimFor the two CDT causal 4-simplex types $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 are unequal, and proves $\alpha_{\min}(4,1)<\alpha_{\min}(3,2)$.
background
This sits in the QG Seven-Gaps Lorentzian-sector lane (Phase 3a), as the threshold layer above the 4D causal-simplex infrastructure. Upstream CausalSimplex4D supplies the CDT-style 4-simplex classes in $D=4$ and the kinematical Wick rotation conventions; the geometric content (squared edge lengths, causal metric data) lives there, not here.
The module's own index type is deliberately thin: a one-field wrapper on a two-constructor enum labeling which causal type is under discussion. It carries no simplices, incidence, or gluing. The two inhabitants are the standard CDT classes $(4,1)$ and $(3,2)$.
WickActionCertAssembly is the neighboring certificate-assembly lane (Wave C4 R5 at $\alpha=1$). Thresholds defined here are the natural cut parameters against which those certificates are read.
proof idea
Definitional core: name the two-value causal-complex index, the two concrete inhabitants, and a threshold extractor that pulls $\alpha_{\min}$ from the causal metric data of each class. Equality lemmas identify the extracted threshold with the named $\alpha_{\min}$ constant for each class.
Comparison layer: prove the two thresholds are distinct, then prove the strict inequality $\alpha_{\min}(4,1)<\alpha_{\min}(3,2)$ by numerical/algebraic comparison (linarith, norm_num style). Admissibility is packaged as a predicate on the Wick-Euclidean side once the threshold is cleared.
No deep geometric construction occurs in-module; proofs are wrappers and ordered comparisons over data imported from the causal-simplex layer.
why it matters in Recognition Science
In the Seven-Gaps gravity campaign this module separates "which causal 4-simplex family" from the metric and certificate work. Downstream certificate and action arguments need a stable name for the Euclidean-admission cutoff of each CDT class; without the ordered pair of thresholds, $(4,1)$ vs $(3,2)$ Wick continuation cannot be stated sharply.
It closes a bookkeeping gap rather than a dynamical one: the forcing-chain landmarks (T7 eight-tick, T8 $D=3$) are ambient RS context, while this file is local to 4D Lorentzian CDT kinematics. No used-by edges are recorded yet, so its consumers are expected in later Wick-action and gap-closure modules that import these thresholds by name.
scope and limits
- Does not construct or glue any 4-simplices; the index is only a two-value label.
- Does not prove dynamical Wick rotation of the gravitational path integral.
- Does not derive continuum Einstein equations or a full CDT measure.
- Does not claim numerical values beyond the ordered comparison of the two thresholds.
- Does not import or depend on the 3D CausalSimplexWick kernel module.
depends on (2)
declarations in this module (25)
-
structure
CausalWickComplex -
def
fourOneComplex -
def
threeTwoComplex -
def
wickContinuationThreshold -
def
wickContinuationThresholdOf -
theorem
wickContinuationThreshold_eq_alphaMin -
theorem
wickContinuationThreshold_fourOne -
theorem
wickContinuationThreshold_threeTwo -
theorem
wickContinuationThresholds_differ -
theorem
wickContinuationThreshold_fourOne_lt_threeTwo -
theorem
causalWickComplex_two_inhabitants -
def
WickEuclideanAdmissible -
theorem
wickEuclideanAdmissible_iff -
theorem
wickEuclideanAdmissible_of_gt_threshold -
theorem
wickEuclideanAdmissible_false_at_threshold -
theorem
wickThreshold_gap_witness -
theorem
wickContinuationThresholdOf_not_constant -
theorem
no_common_typewise_exact_threshold -
theorem
hardcodedConstant_eq_threeTwo_threshold -
theorem
hardcodedConstant_gt_fourOne_threshold -
theorem
joint_wickEuclideanAdmissible_iff -
theorem
universal_sufficient_threshold_eq_max -
theorem
certV2_above_threeTwo_threshold -
theorem
no_certV2_in_fourOne_only_window -
theorem
fourOne_only_window_witness