Schedule
plain-language theorem explainer
A posting schedule is a map from discrete ticks to an optional account–side pair: idle or a single debit/credit post. It is the free dynamical variable of Gap 2; the ledger type and posting rules do not constrain which schedule runs. Downstream reachability and countermodel theorems quantify over this type. The declaration is a pure type synonym.
Claim. For a carrier type $\Lambda$, a posting schedule is a function $\mathbb{N} \to \mathrm{Option}(\Lambda \times \{\mathrm{left},\mathrm{right}\})$: at each tick, either idle or a named account posted on one of the two sides forced by a distinction.
background
Gap 2 asks whether the posting dynamics forces the counts-only premise used in the kind-only cost chain. Earlier arcs showed that neither the cost-function space nor the lattice state type forces counts-only imbalance. This module treats the dynamics layer: posting steps that raise one debit or credit column by one quantum, and runs of those steps.
A schedule is the free input to that dynamics. At tick $n$ it either does nothing or names an account in $\Lambda$ and a side (debit/credit; the two sides of a primitive distinction). The ledger structure fixes how a post updates columns; it does not pick which sequence of posts occurs. Idle ticks leave the state unchanged when the schedule is run forward from the zero ledger.
The module’s committed answer is that the dynamics excludes nothing among nonnegative ledgers: every such ledger is reachable, every integer imbalance is realized, and therefore counts-only is not a theorem about the space of runs.
proof idea
Pure type abbreviation: Schedule Λ is defined as ℕ → Option (Λ × Side). No proof obligations. Side is the two-valued inductive type (left/right) from the primitive recognition calculus; the Option encodes idle versus a single named post.
why it matters
This type is the free variable of Gap 2’s dynamics arc. Theorems such as exists_schedule_of_reachable and imbalance_realized_by_schedule show every reachable nonnegative ledger (hence every integer imbalance) arises from some schedule run from balance. The named premise CountsOnlySchedule is then a property of one schedule’s imbalance path, not a forced law of the dynamics.
The explicit one-post countermodelSchedule on the two-bridge witness lives in this type and witnesses that counts-only fails for a legal run. Downstream, Flight’s eight-gate neutrality and the Searl waveform compliance predicate reuse schedule language for 8-periodic gate sums, tying the same tick-indexed optional-action pattern to the eight-tick octave (T7). The definition therefore anchors both the negative Gap 2 result (dynamics forces nothing) and positive schedule-level invariants elsewhere in the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.