Pith. sign in
module module low

IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeAudit

show as:
view Lean formalization →

Audit leaf for the Wick-action interior-hinge package that freezes the 4D continuation target and the complex-arccos lift. Gravity reviewers of Seven Gaps / Gap-6 design freeze D-gap6-r1 use it to confirm the schema and foundation lemmas N1–N2 are wired. Content is import-and-audit of the hinge module, not a fresh proof chain.

claimAudit module for the frozen four-dimensional Wick-action continuation: the continuation certificate, the terminal claim that the action continues in 4D, and the complex-$\arccos$ lift (continuity on the slit plane off the branch cut, and agreement with real $\arccos$ on $[-1,1]$).

background

Setting is the Seven Gaps gravity stack, Wave C4 R2, under design freeze D-gap6-r1-20260722. Wick rotation continues a classical action from Lorentzian to Euclidean signature. The interior hinge is the analytic glue that replaces real inverse-cosine data by a complex lift so the continued action stays defined off the branch cut.

The imported hinge module freezes that schema: definitions, a continuation certificate type, and a named terminal proposition that 4D Wick continuation holds. It also lands foundation lemmas N1 (slit-plane domain off the arccos cut; continuity of the complex lift on that set) and N2 (the lift restricts to real $\arccos$ on the real interval). This audit module exists to surface that package for review.

proof idea

Definition and audit module, not an independent argument. It imports the interior-hinge development and exposes the frozen schema plus N1–N2. Mathematical work (domain of the complex lift, continuity off the cut, real-restriction identity, certificate packing) lives upstream in the hinge module.

why it matters in Recognition Science

Gives Gap-6 a checkable review surface for 4D Wick-action continuation inside Recognition gravity. The parent feed is the hinge module that freezes the continuation target and the complex-arccos lift (N1+N2). Downstream use is empty: this is a terminal audit leaf, not a lemma that other proofs cite. It keeps the continued action a named proposition with explicit branch-cut foundations rather than an informal analytic aside.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.