QuotientFirstStatus
plain-language theorem explainer
Status record of eight boolean flags for the quotient-first path-sum wave in Seven Gaps Pillar 2. Gravity auditors cite it to read the honesty boundary: object construction, labeled-fiber bridge, excess identity, and non-singleton fibers are green; bounded orbit-stabilizer, continuum limit, substrate 1/|Aut| measure, and gap-1 bridge stay red. Pure structure of Bool fields; no theorem content.
Claim. A status record with eight boolean flags recording whether: the quotient-first path sum $Z_q B(w_q)=\sum_q (1/|\mathrm{Aut}(\mathrm{out}\, q)|)\, w_q(q)$ is constructed; the labeled bridge carries an explicit fiber-cardinality factor; the exact excess relation between labeled $Z$ and $Z_q$ is proved; non-singleton fibers are inherited from the class pushforward; a bounded orbit-stabilizer theorem is derived; an RS continuum limit of $Z$ is obtained; the substrate measure $1/|\mathrm{Aut}|$ is derived rather than modeled; and the gap-1 bridge is derived.
background
Seven Gaps Pillar 2 builds a quotient-first path-sum object promoted by the P2c panel lock. On a triangulation class quotient of a bounded carrier $B$, one defines
$Z_q B(w_q)=\sum_{q:\mathrm{TriangulationClass},B}(1/|\mathrm{Aut}(\mathrm{out},q)|),w_q(q)$,
with finiteness from scoped FiniteQuotient instances on the class pushforward.
The standing labeled path sum with class-constant weight is not unconditionally equal to that quotient sum. It expands as $\sum_q |\mathrm{fiber},q|,\mu(\mathrm{out},q),w_q(q)$, so the difference is the explicit excess $\sum_q(|\mathrm{fiber},q|-1),\mu(\mathrm{out},q),w_q(q)$. Non-singleton fibers are inherited from the class-pushforward edge-class fact, so the fiber factor stays in the bridge.
No full bounded-setoid orbit-stabilizer theorem is supplied in this wave: the carrier ranges over varying signatures, so a single global relabeling action is not available. The $1/|\mathrm{Aut}|$ weight remains a model input until a later derivation.
proof idea
No proof. This is a structure declaration: eight named Bool fields, four of them annotated in-source as false or RED for the present wave. Instantiation and grounding live in the sibling value quotientFirstStatus and its grounding theorem, which pin green flags to kernel lemmas and keep the red flags false.
why it matters
Gives the machine-checkable scoreboard for the quotient-first path-sum honesty boundary inside Gravity / Seven Gaps. Downstream, the canonical instance sets construction, labeled-fiber bridge, exact excess relation, and inherited non-singleton fibers to true, and leaves bounded orbit-stabilizer, $Z$ continuum limit, substrate measure derivation, and gap-1 bridge false.
That matches the module's refusal to resurrect the killed unconditional claim that labeled $Z$ equals the per-class $1/|\mathrm{Aut}|$ sum. In the broader RS gravity stack this is bookkeeping for Pillar 2 of the seven-gap program, not a forcing-chain (T0–T8) step; it records what must still be proved before the quotient object can feed continuum or gap-bridge arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.