quotientFirstStatus_grounded
plain-language theorem explainer
Grounding certificate for the quotient-first path-sum status record: four green flags are tied to the constructed Zq object, the labeled-fiber bridge, the exact excess identity, and the inherited non-singleton fiber at B=2; four red flags stay false. Gravity auditors cite it to lock what Pillar 2c has actually proved versus what remains open. The proof is a pure term packing of rfl on the boolean fields with the four supporting lemmas.
Claim. The quotient-first status record is grounded as follows: the quotient object is constructed and $Z_q(B,w_q)=\sum_q \mu(\mathrm{out}\,q)\,w_q(q)$; the labeled bridge carries the fiber factor so that the standing labeled path sum with class-constant weight equals $\sum_q |\mathrm{fiber}\,q|\,\mu(\mathrm{out}\,q)\,w_q(q)$; $Z_q$ equals that labeled sum if and only if the fiber excess vanishes; the edge class at $B=2$ has fiber cardinality strictly greater than $1$; and the four remaining status bits (bounded orbit-stabilizer, continuum limit, substrate measure, gap-1 bridge) are still false.
background
Pillar 2 of the Seven Gaps gravity program builds a quotient-first path-sum object over triangulation classes. The module constructs $Z_q(B,w_q)$ as the finite sum over TriangulationClass B of the representative symmetry factor $\mu(\mathrm{out},q)$ times the class weight $w_q(q)$. This is the quotient convention, not the standing labeled path-sum measure $Z$.
The honesty boundary is explicit: the P2c panel rejected the unconditional claim that labeled $Z$ equals the per-class $1/|\mathrm{Aut}|$ quotient sum. The exact bridge is $Z_q = Z_{\mathrm{labeled}} + \mathrm{fiberExcess}$, where the excess is $\sum_q(|\mathrm{fiber},q|-1),\mu(\mathrm{out},q),w_q(q)$. Equality holds precisely when that excess vanishes.
Upstream, ClassPushforward supplies fiberCard, the edge complex edgeAB at $B=2$, and the theorem that its fiber has cardinality $>1$. The scalar $\mu$ is the representative symmetry factor pulled from the cost projector stack. No global orbit-stabilizer for the full bounded carrier is derived in this wave.
proof idea
Pure term-mode conjunction. Each green flag is a pair $\langle \mathrm{rfl},,\mathrm{lemma}\rangle$: the boolean field reduces by definitional equality, and the mathematical content is discharged by an already-proved sibling.
- Object constructed:
rflplus definitional unfolding of $Z_q$. - Labeled bridge:
rflpluslabeledZ_eq_sum_fiberCard_mul_mu. - Excess relation:
rflplusZq_eq_labeledZ_iff_fiberExcess_vanishes. - Non-singleton fiber:
rflplusPathSum.one_lt_fiberCard_edgeClass(inherited from ClassPushforward onedgeABat $B=2$).
The four red flags are each closed by a single rfl against the literal false in the status record. No tactics, no new algebra.
why it matters
This is the audit lock for Seven Gaps Pillar 2c. Downstream consumers (none yet wired in the graph) can cite a single theorem rather than re-checking four independent constructions and four open slots. It records, without convention, that the labeled/quotient equality is conditional on vanishing fiber excess, and that the non-singleton fiber at the $B=2$ edge class is why an unconditional identification is unavailable.
Framework role: gravity path-sum bookkeeping on the triangulation quotient, not a forcing-chain (T0–T8) step. The red flags name the remaining scaffold: bounded orbit-stabilizer for varying signatures, the $Z_{\mathrm{RS}}$ continuum limit, a substrate measure derivation, and the gap-1 bridge. Closing any of those requires a separate theorem with explicit gauge/volume hypotheses; this grounding deliberately leaves them false.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.