Index
plain-language theorem explainer
Navigation index for Gap 2's non-equivariant posting verdict: seven boolean flags recording what is settled (posting μ is orbit-mean-one; equivariance supplies constancy; a non-equivariant family posts μ with non-unit numerator; uniqueness wall escaped not breached) and what is not (cost layer determines the measure; measure premise derived). Readers auditing the seven-gaps gravity ledger cite it as a status board. Pure structure definition; no proof content.
Claim. A record type with seven boolean status flags: (i) posting $\mu$ is orbit mean one on the numerator for every letter cost; (ii) equivariance is exactly what upgrades mean one to identically one; (iii) settled: a non-equivariant cost can post $\mu$ with a non-unit numerator; (iv) the witness is a one-parameter family; (v) the witness posted weight is not relabeling-invariant, so the uniqueness wall is escaped not breached; (vi) open: the cost layer determines the measure; (vii) open: the measure premise (unit-sector fugacity / gluing law) is derived.
background
Gap 2 asks when a letter cost posts the RS measure factor $\mu$ on gauge classes of bounded complexes. For equivariant costs, an earlier result closes the route: posting $\mu$ holds exactly when the Boltzmann numerator $\exp(-\mathrm{historyCost})$ is identically one, so the cost layer contributes no extra factor.
This module treats the residual case. Without equivariance, posting $\mu$ is only orbit-mean-one on the numerator (class mass of the posted weight equals $\mu$ iff the numerator totals the orbit cardinality). Equivariance upgrades mean-one to identically-one because it forces the numerator constant on orbits. The open question was whether a non-equivariant cost can still post $\mu$ while individual Boltzmann factors differ.
The module answers affirmatively by a one-parameter tilted family (edge-label transposition with a sign flip under the twist involution). Atom normalizations still hold on complexes with at most one edge letter; non-unit values sit only on classes the sector group moves.
proof idea
No proof: this is a bare structure of seven Bool fields, each annotated by a doc-comment that states the corresponding claim and whether it is settled in the module. The mathematical content lives in the sibling theorem nonequivariant_case_verdict, which packages the five-part conjunction (orbit-mean characterization, equivariant upgrade, existence witness, non-invariance of the tilted posted weight, and unit numerator on $n_E\le 1$ complexes). The index merely labels those verdicts for navigation.
why it matters
Inside the Gravity seven-gaps ledger, Gap 2 is the posting-cost route from letter costs to the measure factor $\mu$. The equivariant half was already closed; this index records that the non-equivariant half is settled in the witness direction by a continuum of tilted costs, without breaching the uniqueness wall (posted weights fail relabeling invariance).
Downstream use count is zero: the structure is a human-facing status board, not a lemma consumed by later proofs. It explicitly flags two remaining open items: that the cost layer determines the measure (the equivariant class admitted one compatible numerator; the full class admits a continuum), and that anything here derives the measure's premise (unit-sector fugacity reducible to the gluing law). A collapse-failure witness is not a derivation. No direct T0–T8 landmark is discharged here; the work is local to the gravity posting layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.