CountsOnlySchedule
plain-language theorem explainer
A posting schedule is counts-only when the imbalance it produces from the zero ledger is kind-constant at every tick: constant on vertices, on edges, and on tetrahedra separately. Gap-2 auditors cite it as the residual physical premise after cost, lattice, and dynamics layers all fail to force counts-only. The body is a universal quantification over ticks of the imbalance-level kind-constancy predicate.
Claim. Given a bounded complex $K$ and a posting schedule $\mathrm{sched}$ on its posting alphabet, $\mathrm{sched}$ is counts-only when, for every tick $t\in\mathbb{N}$, the imbalance configuration of the ledger obtained by running $\mathrm{sched}$ for $t$ steps from balance is kind-constant: there exist integers $c_V,c_E,c_T$ such that the imbalance equals $c_V$ on every vertex letter, $c_E$ on every edge letter, and $c_T$ on every tetrahedron letter.
background
Gap 2's measure chain reduces size-blind weight to kind-only cost, kind-only cost to counts-only charge, and counts-only charge to counts-only lattice imbalance and magnitude. Prior arcs showed none of those premises is forced at its own layer. This module asks whether the posting dynamics forces the imbalance half.
A schedule is a free map from ticks to optional (account, side) posts: the ledger structure does not constrain it. Running a schedule from the zero ledger yields a sequence of ledgers; phiAfter extracts the integer imbalance of the state at tick $t$. Counts-only imbalance means that charge is constant within each geometric kind (vertices, edges, tetrahedra) on the complex's posting alphabet.
The dynamics reaches every nonnegative ledger from balance, hence every integer imbalance, including non-kind-constant ones. Magnitude is silent under posting (ledgers have no magnitude field). What remains as a live premise is therefore a law about the actual run, not a theorem about the space of runs.
proof idea
Definitional abbreviation, not a proved statement. The predicate is the pointwise universal quantification: for every natural-number tick $t$, the imbalance of the ledger after running the schedule $t$ steps from balance satisfies counts-only imbalance on $K$. No tactics or lemmas are applied; the body simply composes the schedule-evolution map with the already-defined kind-constancy predicate on imbalance configurations.
why it matters
This is the named residual premise of Gap 2 after the dynamics arc. The countermodel theorem shows an explicit schedule on the two-bridge witness whose imbalance after one tick is $1$ on edge letter $0$ and $0$ on edge letter $1$, so the predicate fails and counts-only is not forced by dynamics. The three-layer no-go packages that failure with the cost-space and lattice failures: the ledger forces counts-only at no layer examined.
Downstream, the incidence-silence verdict re-exports the no-go and records the string name of this schedule law as the physical premise that remains when dynamics fails. The measure-selection story therefore bottoms out in a law about nature's actual posting run, not a derivable constraint on the space of runs. No T0–T8 forcing step is claimed here; the declaration sits in the gravity Gap-2 scaffolding that isolates which premises must be supplied rather than proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.