Index
plain-language theorem explainer
Hand-curated navigation ledger for Gap 2: whether posting structure plus the gluing law force unit-sector fugacity. Boolean flags mark settled negatives (posting+gluing leave fugacity free; no mu-posting countermodel; tilted family glues at unit fugacity) and two open underivability claims. Gravity auditors cite it to read the Gap-2 status board without chasing theorem names. Fields are assigned by hand; evidence lives in the named theorems, not in projections.
Claim. A navigation record of eight Boolean status flags for Gap 2 on unit-sector fugacity. Settled flags record: (i) the unit-sector premise is equivalent to class mass equaling the projector coefficient $\mu$ at the three atoms and to atom normalization; (ii) the kind-rate posting family coincides with the gluing residue of three positive constants; (iii) posting plus gluing do not force unit fugacity; (iv) no cost that posts $\mu$ is a non-unit-fugacity countermodel; (v) the tilted family glues with unit fugacity. Two flags remain unset: that unit fugacity is derived from posting+gluing, and that it is shown underivable in general.
background
Gap 2 asks whether the posting layer together with the carrier gluing law forces unit-sector fugacity for the path-sum measure. The gluing derivation reduces residual freedom of a size-blind weight to three positive constants (one fugacity per index type); unit sector fugacity is the hypothesis that those constants equal one at the three atoms, equivalently that the labeled weight is normalized there.
The posting layer says a letter cost posts the projector coefficient $\mu$ exactly when the Boltzmann numerator has orbit-mean one. A continuum of non-equivariant tilted costs meets that criterion. The open question this module answers is whether adding the gluing law collapses the three constants to one.
The answer is negative: the kind-only equivariant character costs charge $-\log u$, $-\log v$, $-\log w$ on vertex, edge, and tetrahedron letters. Their posted weight is exactly the size weight of the corresponding character size, they glue at every eligible pair for every positive triple, and their fugacity is unit if and only if $u=v=w=1$. Gluing constrains the shape of the fugacity (it must be a character) and nothing about its value.
proof idea
Not a proved theorem: a structure whose eight Boolean fields are filled by hand as a status board. Each field's docstring points at the named theorem that supplies the evidence; the structure itself carries no proof obligation beyond inhabitation. Settled flags correspond to theorems already in this module and its import (character-cost gluing and posting identification, unit-fugacity iff $\mu$ at atoms, continuum of kind-only equivariant countermodels). The two negative flags for derivation and general underivability are left as explicit non-claims.
why it matters
Closes the Gap-2 ledger in the gravity seven-gaps program: posting plus gluing do not force unit-sector fugacity, and the countermodel is the best-behaved cost in the formalism (kind-only, gauge-equivariant character costs). That negative is exact: the gluing law forces the fugacity to be a character and leaves its value free. What does force unit fugacity is a restatement of the conclusion (class mass equals $\mu$ at the three atoms, or atom normalization).
No downstream consumers are wired yet; the record is the audit surface for the module. It separates settled structure (kind rates equal the three-constant residue; no $\mu$-posting countermodel; tilted family glues at unit fugacity) from the two claims that remain open or refuted on this route: derivation of unit fugacity from posting+gluing alone, and a general underivability theorem. Framework contact is local to the gravity measure construction rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.