the
plain-language theorem explainer
Names the residual open case after the Gap-2 uniqueness wall: label-asymmetric structure on the posting layer is not excluded, and such structure exists, yet no label-asymmetric derivation of label indifference is presently available. Gravity and gauge-counting readers cite it to bound what the pinned-carrier and equivariant-cost theorems actually rule out. It is a structure declaration (definitional packaging), not a proved exclusion.
Claim. Among routes left open by the Gap-2 uniqueness wall, label-asymmetric structure (a cost or weight that distinguishes labels) is not covered by the wall, and such structure exists. What is missing is a label-asymmetric derivation of label indifference; that is the named open case. Premise-level derivations of the Gibbs weight from symmetric first principles lie outside the letter-cost class and are disclosed separately in the module header.
background
Gap 2 (Track A1.2) asks whether the gauge-counting principle can be derived from substrate structure richer than counting at the posting layer. The module's committed answer is no, split into three parts: what the pinned carrier contains, the uniqueness wall that excludes enrichments, and the routes the wall does not touch.
On the pinned carrier, histories are pinned to the balanced zero dual-entry state so the count equals the complex count and every state-factored weight is a function of the complex alone. The uniqueness wall then says that among relabeling-invariant labeled weights, the gauge-counting principle holds for class mass iff the weight is exactly the Gibbs weight; at the cost layer, an equivariant letter cost posts $\mu$ iff its Boltzmann numerator is identically one. No invariant enrichment and no equivariant cost can therefore derive the principle from richer structure.
Part three isolates what those theorems do not quantify over. One untouched route is label-asymmetric structure: costs or weights that break relabeling symmetry. The other is premise-level justification of the Gibbs weight itself from indifference, exchangeability, or maximum entropy.
proof idea
No proof body: this is a structure declaration (def_or_abbrev packaging) that records the residual open case in the module's boundary claim. It does not apply lemmas; it codifies the prose boundary already fixed by the uniqueness theorems on invariant weights and equivariant letter costs, and by the pinned-carrier count identities one level up. Downstream readers treat it as a named hole, not as a discharged theorem.
why it matters
Closes the honest scoping of Gap 2's "no" answer: the uniqueness wall and pinned-carrier theorems exclude only weight-based, relabeling-invariant (or equivariant-cost) routes to the gauge-counting principle. Without this boundary object, a referee could read the wall as a total no-go. The module header and this structure keep two routes explicitly open: (i) label-asymmetric structure, which exists but currently supplies no derivation of label indifference, and (ii) premise-level Gibbs justifications outside the letter-cost class.
In the broader Recognition stack this sits under the gravity seven-gaps program rather than the T0–T8 forcing chain; it protects the claim that posting-layer counting cannot be enriched into gauge counting without smuggling the Gibbs premise, while refusing to overclaim against asymmetric or pre-Gibbs routes. The named open case is exactly the missing label-asymmetric derivation of label indifference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.