PostingAlphabet
plain-language theorem explainer
The posting alphabet of a labeled bounded complex is the disjoint union of finite index sets for its vertices, edges, and tetrahedra. One letter per incidence cell, nothing else. Gauge-counting and dynamics lemmas cite it as the carrier of posted histories and imbalance maps. The body is a three-sum type abbreviation, not a proof.
Claim. For a bounded complex $K$ (with fixed bound $B$), the posting alphabet is the type $\mathrm{Fin}\, n_V(K)\,\oplus\,\mathrm{Fin}\, n_E(K)\,\oplus\,\mathrm{Fin}\, n_T(K)$: one letter per vertex index, edge index, and tetrahedron index.
background
Module Wave C1 R5 builds a gauge-counting measure from posted-history presentations of labeled bounded complexes. A posted bounded history carries incidence indices as letters of a posting alphabet over a dual-entry ledger state; history relabeling is posting-alphabet gauge redundancy. The class measure is $\nu(c)=(#$ histories presenting $c)/($history gauge volume of $c)$, proved to satisfy the gauge-counting principle by explicit bijections, never by defining $\nu$ to be orbit mass.
The dual-entry columns anchor the substrate reading, but arbitrary dual-entry fields would inflate history counts. Counted histories therefore pin the dual-entry state to the canonical balanced zero state (debit = credit = 0, mag = 0). The alphabet itself is deliberately thin: only vertex, edge, and tet indices, so the counting identity does not suffer universe or field inflation.
Upstream census observables $n_V$, $n_E$, $n_T$ supply the three finite cardinalities. Ledger balance and dual-entry strain appear later as state on this alphabet, not as part of the letter set.
proof idea
Definitional abbreviation only. The type is the ternary disjoint sum of finite types of sizes equal to the complex's vertex, edge, and tetrahedron counts. No lemmas, no tactics: the right-hand side is the meaning.
why it matters
This alphabet is the discrete carrier for Gap-2 gauge history and for the dynamics-kind countermodel arc. Downstream, schedules are maps from ticks into optional (letter, debit/credit) pairs on it; imbalance configurations are integer-valued maps on it; counts-only imbalance means the charge is constant on each kind block (all vertices, all edges, all tets).
The two-bridge countermodel posts single edge letters (cmEdge0, cmEdge1) and builds a one-post schedule whose imbalance is incidence-shaped, not kind-constant. The theorem that dynamics produces the incidence countermodel quantifies over ledgers and dual-entry states on this alphabet, showing the counts-only premise is a physical law about the executed schedule, not a consequence of the dynamics space.
In the Recognition gravity stack this is the letter set that keeps residual R5 counting honest: present-and-pinned dual-entry substrate without Aut/$\mu$ in the definitional layer of $\nu$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.