schedule_neutrality_report
plain-language theorem explainer
This definition supplies a string formatter that turns a source into a pass/fail report on schedule neutrality. Engineers integrating LNAL reports into URC adapters would invoke it to surface BALANCE/8 and VECTOR_EQ checks. The body is a direct wrapper: it calls ScheduleNeutralityCert.fromSource and branches on the ok flag to emit either a fixed success string or an error list.
Claim. Given a source string $s$, the report returns the literal string ``OK: Schedule neutrality checks pass (BALANCE/8, VECTOR_EQ/1024, FLIP present)'' when the derived certificate is valid and otherwise the string ``FAIL: '' concatenated with the semicolon-separated error list.
background
Atomicity.Schedule is a structure holding an ordered list of events with pairwise distinctness, representing a one-per-tick history. TimeEmergence.present extracts the current ledger snapshot from a state function. Superhuman.TechnologicalAccess.Schedule is an abbreviation for Fin 8 → ℤ whose neutrality constraint requires the sum over any aligned 8-tick window to vanish. LNALCerts.ScheduleNeutralityCert packages a Boolean ok flag together with an error list and exposes a verified proposition. The LNALReports module sits inside the URC adapter layer and supplies human-readable strings for these certificates.
proof idea
The definition is a one-line wrapper. It invokes ScheduleNeutralityCert.fromSource on the input string, then uses a simple if-then-else to select either the fixed OK message or the FAIL string built by String.intercalate on the error list.
why it matters
The declaration closes the reporting surface for schedule checks that enforce the eight-tick octave neutrality (T7). It feeds the LNAL compiler pipeline by turning the ScheduleNeutralityCert structure into console output, even though no downstream theorem currently consumes the string. The function therefore sits at the boundary between the formal certificate and practical verification tooling inside the Recognition monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.