Pith. sign in
def

zqPhaseStructureStatus

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

plain-language theorem explainer

Canonical status ledger for the quotient-first path-sum phase structure on $Z_q$. It marks four fixed-cap structure results closed (explicit phase model, modulus bound, conditional pairing cancellation, $B=2$ non-vacuity) and three continuum/substrate items open. Anyone tracking Seven Gaps Lane D3 cites it as the single source of truth for what is kernel-proved versus RED. The body is a pure record of boolean flags.

Claim. The status record for the $Z_q$ phase-structure program asserts: an explicit relabeling-invariant phase model exists; the phased path sum is well-defined and modulus-bounded at every fixed complexity cap; conditional exact-opposite pairing cancellation (improving the triangle bound) is proved; a concrete non-vacuous pairing witness exists at cap $B=2$; the continuum limit of $Z_{\mathrm{RS}}$, oscillatory-regulator removal, and a derived substrate phase remain open (false).

background

Lane D3 of the Seven Gaps gravity program works on the quotient-first object $Z_q$: a finite sum over triangulation classes at complexity cap $B$, rather than labeled complexes. This module equips that sum with an oscillatory phase model: a real phase on labeled configurations that is invariant under relabeling, hence descends to classes, with phased weight $e^{i\theta}$ of unit modulus.

At fixed $B$ the phased sum is a finite complex number with $|Z_q| \le$ total class mass $\le$ number of classes. Under an exact-opposite pairing hypothesis (an injection sending a subfamily of classes to partners whose measured summands cancel), the paired mass drops out exactly and the modulus bound strictly beats the triangle inequality whenever the paired family is nonempty. A concrete witness at $B=2$ (phase $0$ on the vertex-free class, phase $\pi$ elsewhere) discharges those hypotheses on two unit-symmetry classes.

The status structure is the module's claim ledger: each boolean names one of those kernel facts, or a RED open item (continuum limit, regulator removal, substrate phase).

proof idea

Definitional record construction, not a proof. Each field of the status structure is assigned a literal true or false Bool corresponding to whether the matching kernel theorem (or witness) exists in this module. No tactics, no lemmas applied at this site; the grounding theorem downstream is what ties the true flags back to the actual statements.

why it matters

This is the single machine-readable claim board for Lane D3 phase structure. The downstream grounding theorem zqPhaseStructureStatus_grounded consumes it and proves every true flag is backed by a kernel statement (phase model and unit-modulus weight for all caps; fixed-cap well-definedness; the general conditional pairing decomposition and strict triangle improvement, not merely the witness; and the discharged $B=2$ pairing witness chain), while the three RED flags stay false.

In the broader Seven Gaps gravity stack it separates what is closed at finite complexity (structure theorems and a non-vacuous cancellation example) from what remains open toward a continuum or substrate-derived phase. It does not itself touch T0–T8 forcing, RCL, or the $\varphi$-ladder mass formula; its role is local bookkeeping so later continuum or ILG kernel work can cite a stable proved/open split.

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