Pith. sign in
structure

WickActionCutLimitFamilyStatus

definition
show as:
module
IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamily
domain
Gravity
line
620 · github
papers citing
none yet

plain-language theorem explainer

Status ledger for Wave C4 F1: the parameterized Wick cut-limit family on the causal range α > 7/12. Six Booleans record which F1 subclaims (cut limit, Lorentz anchor, rapidity pin, Ioc continuity) are closed and whether F2 assembly and gap-6 Lorentzian action remain open. Downstream code builds one concrete instance. Pure structure; no proof content.

Claim. A six-field Boolean record tracking closure of the parameterized Wick cut-limit family for causal $\alpha > 7/12$: whether the cut-limit family, Lorentz-anchor family, rapidity-pinning family, and half-open-interval continuity are closed, and whether F2 assembly and the gap-6 Lorentzian action remain open.

background

Module Wave C4 F1 generalizes the fixed-$\alpha=1$ six-lemma route in WickActionCutLimit to the full causal range $\alpha > 7/12$. All arguments are pointwise in $\alpha$; there is no uniform-in-$\alpha$ bound because the Lorentz factor $k(\alpha)\to 1$ as $\alpha\to\infty$.

The Lorentz factor $k(\alpha)$ (sibling lorentzK) is the hyperbolic cosine of the rapidity pinned by the causal hinge path. The cut-limit log argument approaches $u_0(\alpha)=-k+\sqrt{k^2-1}$ from the upper half-plane as the path parameter $t\downarrow 0$. Continuity and branch choices for $\mathrm{csqrt}$ and $\mathrm{Log}$ are handled by the sibling tendsto lemmas.

This structure does not itself inhabit the F2 continuation certificate or flip any ledger Bools (F3). It only names the status fields those later stages will read.

proof idea

Definition only: a structure with six Bool fields and no constructors beyond the default. No tactics, no lemmas applied. The sole downstream inhabitant fills the fields by literals (true for the four F1 closures, false for F2 assembly open; gap-6 left as supplied).

why it matters

Gives the typed ledger that wickActionCutLimitFamilyStatus inhabits, marking F1 cut-limit, Lorentz-anchor, rapidity-pin, and Ioc-continuity closed while leaving F2 assembly open. That instance is the Wave C4 F1 handoff into the Seven Gaps gravity stack (binding design D-gap6-v2-succession-family).

In the broader RS gravity program this is scaffolding for gap-6 Lorentzian action via Wick rotation of the pentagonal hinge path. It does not yet discharge gap-6 itself; F2 assembly and the Lorentzian-action Bool remain the open gates. No direct T0–T8 forcing step; the link is through the causal rapidity and eight-tick geometry already fixed upstream.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.