quotientFirstStatus
plain-language theorem explainer
Canonical Bool status snapshot for the quotient-first path-sum wave (Seven Gaps, Pillar 2). It marks four closed items: object constructed, labeled bridge with fiber factor, exact excess relation, and inherited non-singleton fibers; four remain false: bounded orbit-stabilizer, continuum limit of Z_RS, substrate measure, and gap-1 bridge. Gravity auditors cite it to read what this module actually closed versus what it refuses. The body is a pure record literal of flags.
Claim. The quotient-first status record is the Boolean tuple with: quotient-first object constructed $=\mathrm{true}$; labeled bridge carries a fiber factor $=\mathrm{true}$; exact excess relation proved $=\mathrm{true}$; non-singleton fiber fact inherited $=\mathrm{true}$; bounded orbit-stabilizer derived $=\mathrm{false}$; continuum limit of $Z_{\mathrm{RS}}=\mathrm{false}$; substrate measure derived $=\mathrm{false}$; gap-1 bridge derived $=\mathrm{false}$.
background
Pillar 2 of the Seven Gaps gravity program builds a quotient-first path-sum object promoted by the P2c panel lock. For a bounded triangulation carrier $B$ and a class-constant weight $w_q$, the quotient sum is
$$Z_q(B,w_q)=\sum_{q}\frac{1}{|\mathrm{Aut}(\mathrm{out},q)|},w_q(q),$$
with the finite quotient supplied by scoped FiniteQuotient instances from the class-pushforward layer.
The standing labeled path sum is not unconditionally equal to this $1/|\mathrm{Aut}|$ form. With a class-constant weight it expands as a fiber-weighted sum $\sum_q |\mathrm{fiber},q|,\mu(\mathrm{out},q),w_q(q)$. Their difference is the explicit excess $\sum_q(|\mathrm{fiber},q|-1),\mu(\mathrm{out},q),w_q(q)$, so equality holds if and only if that excess vanishes. Non-singleton fibers are inherited from the class-pushforward edge-class fact, so the fiber factor stays in the bridge.
The status structure is the module's honesty ledger: green flags name what was constructed or proved; red flags name what this wave deliberately does not claim (no full bounded-setoid orbit-stabilizer, no continuum limit, no substrate measure, no gap-1 bridge).
proof idea
Pure definitional record. Each field of the status structure is assigned a concrete Boolean: the four closed items true, the four open or refused items false. No tactics, no lemmas, no computation beyond the literal. The companion grounding theorem later ties the true flags to the constructed $Z_q$ object, the fiber-factor bridge, the excess identity, and the inherited non-singleton fiber theorem, while keeping the red flags false.
why it matters
This record is the audit surface for the quotient-first wave. Downstream, the grounding theorem binds every green flag to a kernel statement (constructed $Z_q$, labeled bridge with fiber factor, exact excess relation, inherited non-singleton fibers) and keeps the red flags false, recording why unconditional labeled/quotient equality is unavailable.
In the Recognition gravity stack it enforces the P2c honesty boundary: the panel killed the claim that the standing labeled path-sum measure equals the per-class $1/|\mathrm{Aut}|$ quotient sum, and this file does not resurrect that claim by convention. The missing orbit-stabilizer for the full bounded triangulation-class setoid is explicit; unlike fixed-signature exact-shell machinery, the bounded carrier ranges over varying signatures, so no single global relabeling action is supplied here. Future orbit-stabilizer work must state signature/gauge-volume hypotheses openly. The continuum-limit and substrate-measure reds mark open interfaces toward a continuum $Z_{\mathrm{RS}}$ and a derived measure on the substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.