index_no_countermodel
plain-language theorem explainer
Certifies that the Gap-2 fugacity-posting-gluing status index sets its no-mu-posting-countermodel flag to true. Gravity auditors tracking the Seven Gaps ledger cite this as the boolean seal on that slot. The proof is pure reflexivity against the index record.
Claim. In the Gap-2 fugacity-posting-gluing status index, the flag recording that there is no countermodel to $\mu$-posting equals $\mathrm{true}$.
background
Gap 2 asks whether the posting layer together with the gluing law force unit sector fugacity for the path-sum measure. The module answer is negative: residual freedom after gluing is three positive constants (one fugacity per index type), realized by characterSize, and unit fugacity is an extra premise, not a consequence.
Posting $\mu$ means the Boltzmann numerator has orbit-mean one. Gap2NonEquivariantPosting already showed that criterion is exactly orbit-mean one and is met by a continuum of costs, including non-equivariant ones. This module's best-behaved countermodel is the kind-only gauge-equivariant character cost, whose posted weight is exactly the size weight of the three-constant residue and which glues at every eligible pair, yet has unit fugacity only when all three constants are one.
Status is collected in a boolean Index record. Sibling modules (dynamics kind rule, non-equivariant posting, posting-layer floor) expose the same pattern: a structure of named flags set to true when the corresponding claim is settled in that file.
proof idea
One-line reflexivity. The local index definition hard-codes no_mu_posting_countermodel := true among its fields; the theorem is rfl against that field projection. No lemmas are applied.
why it matters
Closes the bookkeeping entry for the mu-posting side of Gap 2 inside the Seven Gaps gravity program. The module's substantive finding is that posting plus gluing constrain only the shape of the fugacity (it must be a character) and leave its value free; the matching index flags include posting_plus_gluing_leaves_fugacity_free and this no-countermodel seal on mu-posting itself.
Downstream use is empty so far: the theorem is a ledger stamp, not an input to further proofs. It sits beside the equivalences that restate unit fugacity as class mass equaling $\mu$ at the three atoms, and as normalization of the labeled weight there. Those restatements, not posting-plus-gluing, are what force the unit-sector premise the Gap-2 measure rests on.
No direct T0-T8 or RCL citation; this is infrastructure inside the gravity gaps stack, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.