// std/kot.neb
// Kase Optimality Theorem — governance self-description.
//
// A canonicalization is optimal iff:
// Minimal: no step can be eliminated
// Complete: no rule fires on the terminal
// Consistent: no confluence failure exists at the source
//
// The KOT verdict IS a Trit:
// P = optimal
// N = not optimal
// Z = indeterminate (not yet checked)
//
// SELF-HOSTING BOUNDARY:
// The bridge predicates dissolve in Session 004 when
// span arithmetic and ordering are expressible in .neb.
// What remains will be pure governance.
type step = { } // any rewrite step
type optimal = { } // any Geoit under KOT scrutiny
// Minimality: a step is necessary if removing it changes the terminal.
// Bridge: 'necessary' — checks replay equivalence. Session 004.
for s : step where necessary(s) => s * minimal = s
// Completeness: the terminal has no applicable rules.
// Bridge: 'terminal' — checks rule applicability. Session 004.
for t : optimal where terminal(t) => t * complete = t
// Consistency: no confluence witness exists at the source.
// Bridge: 'confluent' — runs explore_confluence. Session 004.
for g : optimal where confluent(g) => g * consistent = g