ScheduleNeutralityCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not establish the eight-tick rotation lemma.
- Does not apply outside the eight-tick invariant assumption.
- Does not perform cost algebra computations.
- Does not validate against the full Recognition forcing chain.
formal statement (Lean)
114structure ScheduleNeutralityCert where
115 ok : Bool
116 errors : List String := []
proof body
Definition body.
117deriving Repr
118
119@[simp] def ScheduleNeutralityCert.verified (_c : ScheduleNeutralityCert) : Prop :=
120 ∀ (P : IndisputableMonolith.LNAL.LProgram)
121 (s : IndisputableMonolith.LNAL.LState),
122 IndisputableMonolith.LNAL.EightTickInvariant P s →
123 ∃ r, r ≤ 7 ∧ ∀ k,
124 (Function.iterate (IndisputableMonolith.LNAL.lStep P) (r + 8 * k) s).winIdx8 = 0 ∧
125 (Function.iterate (IndisputableMonolith.LNAL.lStep P) (r + 8 * k) s).winSum8 = 0
126
127@[simp] theorem ScheduleNeutralityCert.verified_any (c : ScheduleNeutralityCert) :
128 ScheduleNeutralityCert.verified c := by
129 intro P s H
130 simpa using IndisputableMonolith.LNAL.schedule_neutrality_rotation (P:=P) (s:=s) H
131
132def ScheduleNeutralityCert.fromSource (src : String) : ScheduleNeutralityCert :=
133 let parsed := parseProgramFull src
134 let emptyPhi : PhiIR.PhiAnalysis := { literals := #[], errors := #[], duplicateNames := [] }
135 let emptyPackets : PhiIR.PacketAnalysis := {}
136 let code := match parsed with
137 | .ok out => out.code
138 | .error _ => #[]
139 let phi := match parsed with
140 | .ok out => out.phi
141 | .error _ => emptyPhi
142 let packets := match parsed with
143 | .ok out => out.packets
144 | .error _ => emptyPackets
145 let rep := staticChecks code phi packets
146 { ok := rep.ok, errors := rep.errors }
147
148/-- Cost ceiling certificate (|net GIVE−REGIVE| ≤ 4 per 8‑tick window). -/