Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly

show as:
view Lean formalization →

Assembly module for the 4D Wick-action continuation certificate on the three-pent interior-hinge complex. It packages cut-limit, Euclidean Schläfli, and interior-hinge lemmas into the V2 certificate and the pointwise carccos value at the Lorentzian cut. Gravity/QG workers cite it when discharging the frozen gap-6 continuation schema. Structure is lemma assembly plus a few explicit real/complex evaluations, not a single deep proof.

claimOn the minimal three-pent one-hinge complex, the module records the principal value of the complex arccosine at the Lorentzian cut cosine, the cut-boundary limit of that path, and assembles the certificate $\mathrm{WickActionContinuationCertV2}$ asserting that the real part of the Wick action path is differentiable at the Euclidean endpoint $\alpha$ whenever $\alpha>7/12$, with the causal edge-length assignment held fixed.

background

The QG Seven-Gaps campaign treats 4D causal (CDT-style) simplices and the kinematical Wick rotation of Regge hinge data. Upstream, CausalSimplex4D fixes the 4-simplex classes; ThreePentCausalConsistency supplies an admissible causal edge-length assignment on the minimal interior-hinge complex; WickActionComplexFirst starts the complex-first formalization of the Lorentzian Wick arc.

The complex arccosine carccos is the analytic engine: its slit-plane continuity and real restriction to ordinary arccos are banked in the interior-hinge module, while WickActionCutLimit lands the cut-boundary limit at cosine one via a six-lemma route. Euclidean Schläfli variation at the Wick endpoint is the remaining analytic ingredient (existence of a real derivative of the real part of the action path in the Euclidean angle).

This module sits at the assembly layer: it evaluates concrete constants (e.g. $\sqrt{57}/8$, $\mathrm{acosh}(11/8)$), records pointwise cut values, and packages the frozen certificate schema rather than inventing new geometry.

proof idea

Not a single theorem proof. The module evaluates explicit real and complex special values (square roots, arcosh, carccos at the Lorentz cut), proves elementary non-equalities such as the zero-path action differing from the Lorentz limit, and continuity/tendsto lemmas on half-open intervals. It then assembles those facts with the imported cut-limit, Schläfli, and hinge lemmas into WickActionContinuationCertV2 and the family/at-one specializations. Several results are short norm_num/linarith/ring discharges or one-line applications of upstream continuity statements.

why it matters in Recognition Science

Closes the Wave C4 assembly step for the action-level Wick certificate on the fixed three-pent threeTwo complex. Downstream, WickActionCertFamilyAssembly consumes the banked V2 ingredients to build wickActionContinuationCertV2_of_causal under $\alpha>7/12$ and land the succession terminal. WickActionCertAssemblyAudit checks that headline theorems stay inside [propext, Classical.choice, Quot.sound] with zero sorryAx. WickActionComplexFamilyThreshold then converts the hardcoded $\alpha>7/12$ range into a structural finding that the threshold is complex-dependent, answering the referee objection that the constant is not complex-independent. Within Recognition gravity, this is the hinge between kinematical Wick rotation and a certifiable Regge action path in the Lorentzian sector.

scope and limits

used by (3)

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

depends on (9)

Lean names referenced from this declaration's body.

declarations in this module (24)