phiAfter
plain-language theorem explainer
The imbalance map after t ticks of a posting schedule started from the balanced zero ledger. Anyone working the Gap-2 dynamics arc cites it when stating counts-only as a property of runs, or when exhibiting schedules that realize a target imbalance. The body is a one-line composition: run the schedule from zero, then take Recognition.phi of the resulting ledger.
Claim. For a posting schedule $\mathrm{sched}$ on carrier $\Lambda$ and a tick count $t\in\mathbb{N}$, write $\phi_{\mathrm{after}}(\mathrm{sched},t):\Lambda\to\mathbb{Z}$ for the imbalance of the ledger obtained by running $\mathrm{sched}$ for $t$ steps from the balanced zero ledger (every debit and credit column empty).
background
Gap 2 asks whether posting dynamics force the counts-only premise on charges. A schedule is a free map from ticks to either idle or a named account posting on a named side (debit or credit). Running a schedule from an initial ledger applies those posts in order; idle ticks leave the state fixed.
The balanced zero ledger has every column empty and is the initial condition of the dynamics (histories pinned by the canonical-history constraint, now read as a start state). Recognition.phi extracts the integer imbalance of a ledger (debit minus credit, per account). The module's committed answer is that dynamics exclude nothing among nonnegative ledgers, so every integer imbalance arises as phi of a reachable state.
Upstream, runSchedule is the recursive stepper: at 0 return the seed; at t+1 either stay put on idle or apply one post. phiAfter packages the standard initial-condition choice (zero ledger) with that stepper and the imbalance readout.
proof idea
Definition, not a proof. Body is the composition Recognition.phi (runSchedule zeroLedger sched t): start at the balanced zero ledger, advance the schedule for t ticks, read off the imbalance map. No lemmas are applied; the meaning is entirely inherited from runSchedule, zeroLedger, and Recognition.phi.
why it matters
This is the standard imbalance observable along a dynamical run, and it is where the counts-only premise is restated at the schedule layer. CountsOnlySchedule requires that phiAfter sched t be kind-constant at every tick; that is the named premise the module shows is not forced by dynamics.
Downstream, imbalance_realized_by_schedule states that every map φ : Λ → ℤ equals phiAfter sched t for some schedule and tick, the schedule form of full imbalance reachability. The countermodel theorem schedule_countermodel_not_countsOnly evaluates phiAfter on an explicit one-tick schedule on the two-bridge witness and shows the resulting imbalance is not kind-constant. The module index records the same fact as every_imbalance_realized_by_schedule.
In the Gap-2 chain this closes the dynamics arc: cost, lattice state, and now posting dynamics all fail to force counts-only; what remains is a physical premise about the actual run the universe executes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.