CostSizeBlind
plain-language theorem explainer
Size-blindness for a letter cost means the total history charge depends only on the three cell counts (vertices, edges, triangles). Gap-2 posting-layer arguments cite this predicate when relocating premise (i) from labeled weights onto costs. It is a Prop definition, not a proved claim: matching counts force equal summed letter costs. Downstream witnesses such as the vertex-pair charge discharge it at use sites.
Claim. A letter cost $c$ is size-blind if, for any two bounded complexes $K$ and $L$, equality of the three counts $n_V(K)=n_V(L)$, $n_E(K)=n_E(L)$, and $n_T(K)=n_T(L)$ implies equality of history costs: the sum of letter charges on $K$ equals the sum on $L$.
background
Gap 2 in the gravity seven-gaps program asks how premise (i), size-blindness of a labeled weight, can be obtained from a posting presentation rather than assumed. The module works at the posting layer: a complex is read as a history of letters from a three-block alphabet (one letter per vertex, edge, and triangle cell). A letter cost assigns one real to each such letter at each size cap; nothing here derives a substrate emission process.
History cost is the sum of those letter charges: pure ledger additivity over postings. The posted weight is the Boltzmann factor of that cost over the gauge volume $1/(n_V!,n_E!,n_T!)$. At this layer, size-blindness of the weight reduces to the total charge being a function of the three counts alone. This predicate packages that reduction on the numerator cost only.
The companion size-blindness-reach development already showed that indistinguishability premises weaker than the three counts cannot force size-blindness for every weight. The present module attacks premise (i) from the opposite direction: by assigning a cost rather than by failing to separate complexes.
proof idea
Definition, not a proof. The body is a universal Prop: for every pair of size caps and bounded complexes, equality of vertex, edge, and triangle counts implies equality of history costs under the given letter cost. No tactics or lemmas fire here. Discharge happens at use sites by rewriting the history cost into an explicit function of the counts (for example the vertex-pair charge, whose history cost is $n_V(n_V-1)$).
why it matters
This is the posting-layer restatement of premise (i). The nearby theorem comment records the exact content: a posted weight is size-blind precisely when its total charge is a function of the three counts, so the posting presentation relocates premise (i) onto the cost rather than weakening it.
Downstream, the vertex-pair letter cost is proved size-blind and used to show the kind rule fails by counting alone, without incidence structure. That witness feeds the incidence-silence verdict certificate: there exist equivariant size-blind costs that are not fixed-kind-totals. Sibling results also show size-blindness plus atomic letter structure do not force a Gibbs form.
In the Recognition gravity stack, Gap 2 is one of the seven gaps between the recognition ledger and continuum gravitational phenomenology. The predicate is local scaffolding for deriving the measure at the posting layer; it is not a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.