ScheduleNeutralityCert
plain-language theorem explainer
Schedule neutrality certificate aggregates checks for schedule balance in LNAL programs over eight-tick windows. Report generators in the URC adapters cite this structure when producing verification manifests. The definition supplies a boolean flag and error list, with its verified property obtained by direct appeal to a rotation lemma.
Claim. A schedule neutrality certificate consists of a boolean success indicator and a list of error strings. It is verified precisely when, for every program $P$ and state $s$ satisfying the eight-tick invariant, there exists an integer $r$ with $r$ ≤ 7 such that for all integers $k$ the state obtained by iterating the step function $r + 8k$ times has vanishing window index and window sum at scale 8.
background
LNAL invariants certificates bundle virtual machine preservation with token delta-unit bounds. The local setting defines schedule neutrality via checks on program execution over the eight-tick period, where a tick is the fundamental time quantum τ₀ = 1. Upstream results include the iterate combinator for repeated function application and the H reparametrization of the J-cost satisfying H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
The verified property is established by a one-line wrapper that invokes the schedule neutrality rotation lemma and simplifies the resulting expression.
why it matters
The certificate is consumed by the schedule neutrality report generator and the manifest JSON aggregator in the URC adapters. It fills the schedule-related slot in the LNAL invariants bundle, linking directly to the eight-tick octave (T7) of the unified forcing chain. It provides a concrete interface for program-level checks without addressing the underlying functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.