hardcodedConstant_eq_threeTwo_threshold
plain-language theorem explainer
The rational 7/12 equals the Wick Euclidean-admission threshold of the three-two causal 4-simplex type. Gravity and continuum-limit workers cite it when tying the action certificate's hardcoded causal-range literal to the typewise kinematical gate. The proof is a one-line symmetry of the already-proved three-two threshold evaluation; it is arithmetic identity, not a derivation of the constant from alphaMin.
Claim. As real numbers, $7/12$ equals the Wick continuation threshold of the three-two causal complex (three pentachora of one class and two of the other).
background
This module sits in the Pillar 1 strengthen campaign on Wick continuation for causal 4-simplices. The action-level certificate WickActionContinuationCertV2 hardcodes the causal range $\alpha > 7/12$ on a fixed three-pent one-hinge complex of type three-two. Referees objected that this looks like a universal constant; the module answers by making the type dependence explicit.
Kinematical Euclidean admission after Wick is governed by a typewise gate alphaMin on causal 4-simplex types: alphaMin of four-one is $3/8$, and alphaMin of three-two is $7/12$. These are exact (iff) gates for positive continuum measure after Wick. The Wick continuation threshold of a complex is that type's alphaMin, packaged as a function of the complex.
The certificate field causalRange : 7/12 < α is a hardcoded literal in the assembly module. The present identity only matches that literal to the three-two member of the threshold function. The actual projection linking certificates to the gate is the separate theorem that certificates sit above the three-two threshold.
proof idea
One-line term proof: take the established evaluation that the Wick continuation threshold of the three-two complex equals $7/12$, and reverse the equality by symmetry. No arithmetic, no case split, no appeal to four-one data.
why it matters
The identity is the bridge that lets the hardcoded certificate constant be read as the three-two threshold rather than as a mysterious universal number. Downstream, hardcodedConstant_gt_fourOne_threshold rewrites through this fact and the strict inequality of the two type thresholds, proving $7/12$ strictly overstates the four-one gate. That comparison feeds the four-one-only window witness at $\alpha = 1/2$: four-one continues for every positive spacelike scale, yet no action certificate exists because the certificate demands $\alpha > 7/12$ by construction.
In the module's honest split, $7/12$ remains a complex-independent sufficient threshold (it is the max of the two type gates) but is not a complex-independent exact gate. The declaration pins the arithmetic half of that story. It does not close outcome (a): full action-level continuation for a genuine multi-complex family remains a separate campaign; CertV2 stays specialized to the collapsed three-two one-hinge path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.