zqPhaseStructureStatus_grounded
plain-language theorem explainer
Packages the Lane D3 phase-structure status record: every green flag is witnessed by a kernel theorem (phase model, fixed-cap bound, general pairing cancellation, and a concrete B=2 non-vacuity witness), while continuum limit, regulator removal, and substrate-derived phase stay red. Gravity auditors cite it as the single grounded checklist for quotient-first oscillatory Zq. The proof is a pure term package of rfl plus named sibling lemmas.
Claim. The phase-structure status record is grounded: the phase model is defined, and for every complexity cap $B$ and every phase model $P$, the descended class phase equals $P$'s labeled phase and every phased weight has modulus $1$; the phased quotient path sum is bounded by total class mass at fixed cap; under an injective opposite-summand pairing $j$ on a subfamily $s$, $Z_q$ reduces exactly to the unpaired remainder sum; at $B=2$ an explicit witness satisfies $\|Z_q\| \le M-2 < M$ with $M\ge 2$; and the continuum-limit, regulator-removal, and substrate-phase flags remain false.
background
Lane D3 works on the quotient-first path sum $Z_q$ over triangulation classes at fixed complexity cap $B$. A PhaseModel supplies a real phase on labeled bounded complexes that is invariant under relabeling, so it descends to a well-defined class phase; the phased weight is $\exp(i\cdot\mathrm{phase})$ and has unit modulus. The measure factor $\mu$ on class representatives multiplies these weights in the finite sum defining $Z_q$.
The module already proves fixed-cap well-definedness ($|Z_q|\le$ total class mass $\le$ number of classes), conditional exact cancellation when an injection $j$ pairs classes outside a subfamily to opposite measured summands, and two-term arithmetic that equal masses at phases $\theta$ and $\theta+\pi$ cancel strictly better than the triangle inequality. A concrete $B=2$ model (phase $0$ on the vertex-free class, $\pi$ elsewhere) discharges those pairing hypotheses on unit-symmetry classes.
Status flags elsewhere in the file mark which of these kernels are closed versus still open (continuum limit of $Z_{\mathrm{RS}}$, removal of an oscillatory regulator, and a substrate-derived rather than input phase).
proof idea
Pure term-mode package. Each green flag is rfl conjoined with the corresponding kernel fact: classPhase_mk and phasedWeight_norm for the phase-model block; the first conjunct of Zq_phased_wellDefined for the fixed-cap bound; Zq_pairing_decomposition for general conditional cancellation; and the triple phased_Zq_pairing_witness, phased_Zq_beats_triangle_witness, two_le_totalClassMass_two for non-vacuity at $B=2$. The three red flags are closed by rfl against the literal false in the status record. No new arithmetic is performed here.
why it matters
This is the grounding theorem for Seven Gaps Lane D3: it ties every true status bit to a proved kernel statement (the pairing flag to the general conditional theorem, not only the witness) and keeps the open continuum and substrate questions honestly red. Downstream consumers of the status record can trust green means theorem-backed and red means still open.
In the broader Recognition picture this sits on the gravity side of the quotient-first path sum, not on the T0–T8 forcing chain itself. It does not claim a continuum $Z_{\mathrm{RS}}$ limit, does not derive an oscillatory regulator removal, and does not produce a substrate phase from the eight-tick or J-cost structure; those remain explicit open flags. The $B=2$ witness only shows that pairing cancellation is non-vacuous at small cap, so improved bounds below the triangle inequality are attainable in principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.