causalWickComplex_two_inhabitants
plain-language theorem explainer
The causal Wick-complex class contains at least two distinct type labels: the four-one and three-two pent types are unequal. Anyone citing type-dependent Wick thresholds or the four-one-only window needs this separation. The proof unfolds the two package constructors and discharges equality by cases on distinct inductive constructors.
Claim. If $C_{4{+}1}$ and $C_{3{+}2}$ are the two packaged causal Wick complexes built from the four-one and three-two causal pent types, then their underlying types are unequal: $\mathrm{ty}(C_{4{+}1}) \neq \mathrm{ty}(C_{3{+}2})$.
background
This module answers a referee objection to the action-level Wick certificate: the hardcoded causal range $\alpha > 7/12$ is not a complex-independent constant. Kinematical Wick Euclidean admission for causal 4-simplices is already type-dependent through alphaMin on causal pent types, with $\alpha_{\min}(4{+}1)=3/8$ and $\alpha_{\min}(3{+}2)=7/12$, each an exact gate for positivity of the Cayley-Menger quantity cm4 after Wick (sign-normalized so $\mathrm{cm4}>0$ on non-degenerate Euclidean 4-simplices).
The common class packages a causal pent type as a Wick complex. Its two named inhabitants are the four-one complex and the three-two complex. The present lemma records that those inhabitants carry distinct types, so the class is genuinely multi-type rather than a singleton in disguise.
Upstream, cm4 supplies the Euclidean non-degeneracy test; the two complex packages are definitional wrappers around the inductive constructors fourOne and threeTwo.
proof idea
One short tactic proof. Unfold the two complex packages to expose their type fields as the constructors CausalPentType.fourOne and CausalPentType.threeTwo. Assume equality of those constructors and case-split: the inductive type has no identification between them, so the assumption is empty and the goal closes.
why it matters
Without distinct inhabitants, talk of type-dependent thresholds collapses. This lemma underwrites the structural finding that $7/12$ is only the three-two member of the threshold function, while four-one continues down to $3/8$. Downstream, fourOne_only_window_witness uses the multi-type picture to exhibit $\alpha=1/2$ in the open window $(3/8,7/12)$: four-one admits Euclidean continuation for every positive spacelike scale, yet no WickActionContinuationCertV2 exists because that certificate hardcodes $7/12<\alpha$.
In the Gravity/SevenGaps campaign this is the elementary separation step before comparing thresholds, proving they differ, and showing there is no common typewise exact gate. It does not touch the forcing chain (T0-T8) or the Recognition Composition Law; it is local to Wick continuation of causal 4-simplices and the honesty split between sufficient versus exact thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.