Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge

show as:
view Lean formalization →

Defines the complex-first Wick continuation of Regge interior-hinge data: principal complex arccos via a log lift, the pentagonal hinge cosine path, dihedral-sum and area paths, and the Wick action path that interpolates Euclidean to Lorentzian regimes. Gravity/QG campaign consumers cite it for cut-limit, Schläfli, and certificate-assembly work. The module packages definitions and path constructions rather than a single terminal theorem.

claimIntroduce the principal complex arccos $\operatorname{carccos}(w)$ by a log lift with square root only on $1-w^2$; the pentagonal hinge cosine path $c(\alpha,t)$, dihedral-sum and hinge-area paths, and the Wick action path $S_W(\beta,\alpha)$ connecting Euclidean cosine/area/angle data to Lorentzian cosine, rapidity, and real angle, together with the continuation certificate schema binding these fields.

background

This sits in the QG Seven-Gaps Lorentzian-sector lane (complex-first 4D Wick continuation of Regge hinge data, panel C11). Prior discrete-gravity layers were Euclidean; CausalSimplexWick and CausalSimplex4D supply CDT-style causal simplex classes and the kinematical Wick rotation in 3D/4D. ThreePentCausalConsistency supplies an admissible causal edge-length assignment on the minimal interior-hinge complex.

The module's own doc fixes the analytic convention: complex principal arccos is realized by a log lift, and the complex square root is applied only to $1-w^2$, never to cofactor products. Sibling objects include Euclidean and Lorentzian cosine/area/angle readouts, Lorentzian rapidity, the pentagonal hinge cosine path, dihedral-sum and hinge-area paths, the Wick action path, and the WickActionContinuationCert schema that packages the continuation obligations.

CampaignLedger and FullTheoryLedger record scoped increments versus full-strength closures; this module does not flip those flags by itself.

proof idea

Definition-and-path module for the interior-hinge Wick action, not a single terminal proof. It builds carccos from the complex log lift with the restricted csqrt domain, then assembles the geometric paths (pentHingeCosPath, dihedral sum, hinge area, wickActionPath) and the Euclidean/Lorentzian readout maps (cosine, area, angle, rapidity). Certificate fields are exposed as a structured Prop schema for downstream habitation. Analytic work (derivatives, cut limits, confinement) is deferred to importers; local content is the shared analytic and geometric vocabulary those proofs apply.

why it matters in Recognition Science

Feeds the Wave C4 interior-hinge stack. WickActionCutLimit and WickActionCutLimitFamily land carccos cut-boundary limits (six-lemma route at $\alpha=1$, then the $\alpha>7/12$ family). WickActionEuclidSchlaefli inhabits the Euclidean Schläfli / $\alpha$-variation field of the continuation certificate (existence of a real derivative of the Wick action path at the Euclidean endpoint). WickActionCertAssembly compares pointwise carccos values to the N4 one-sided cut limit. WickActionInteriorHingeConfinement closes Moebius confinement and branch-regular-sum shape on the causal $\alpha$-range; the audit module checks axiom footprint.

In the Recognition/QG campaign this is the shared hinge-action substrate for gap-6 Wick continuation: without these paths and the restricted principal-arccos convention, cut limits, Schläfli identities, and certificate assembly have no common formal object. It does not itself close gap-6 terminal Bools or full-theory ledger flags.

scope and limits

used by (6)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (26)