Lnal Vm

The recognition machine

An LNAL VM is a formal model of a computer whose only job is to process recognition events, the discrete acts of pattern-matching that Recognition Science takes as its primitive. The machine is defined in the framework's machine-checked library of formal theorems as a program that reads instructions from a numbered list, executes one at a time, and updates a state. Its state tracks a breath counter, a window index, and budget registers that record how much recognition cost remains available in the current window.

The machine's defining feature is a proved guarantee about its own execution. The library proves a progress theorem: from any state, the machine can always take a step to some next state. It also proves a preservation theorem: after any step, the breath counter stays below its period of 1024, so the machine never runs out of its per-window budget. These two results together establish that the LNAL VM is a total, always-advancing computation, not a partial one that can stall or exhaust its resources.

The machine also models a consent gate, a flag that can be enabled to allow a recognition event to commit. The library defines an eight-beat program built from a k-gate program run twice, and provides trace functions that simulate the machine's execution step by step. These traces are used to check invariants, such as the k-gate increment invariant that verifies the vector sum increases by the expected amount at each step.

In Recognition Science, this VM serves as the concrete substrate on which the framework's derived constants and cycles are meant to run. The eight-tick recognition cycle that the framework derives from its cost function is here realized as an explicit program that can be executed and traced. The VM is the point where the framework's abstract theorems about recognition cost meet a concrete, mechanically checkable execution model.

/-- Progress: every state can take a small‑step (possibly self if halted). -/
theorem progress (P : LProgram) (s : LState) : ∃ s', LStepRel P s s' := by
  exact ⟨lStep P s, lStep_as_rel P s⟩

/-- Preservation (breath bound): stepping keeps breath within period. -/
theorem preservation_breath (P : LProgram) (s : LState) :
    BreathBound (lStep P s) := by
  -- direct from arithmetic lemma
  simpa [BreathBound] using l_breath_lt_period P s

--------------------------------------------------------------------------------
-- Hardware test vectors and invariants
--------------------------------------------------------------------------------

structure LState where
  reg6   : Reg6
  aux5   : Aux5
  ip     : Nat
  breath : Nat
  halted : Bool
  winSum8 : Int
  winIdx8 : Nat
  flipped : Bool
  vecSumCycle : Int
  /-- Per-window J budget (monotone nonincreasing across a window). -/
  jBudgetWin : Nat
  /-- Configured per-window budget allowance (reset target when the window rolls). -/
  jBudgetMax : Nat := 4
  /-- Historical record of closing budgets for completed windows (most recent last). -/
  jBudgetHistory : List Nat := []
  /-- Count of completed 8-op windows. -/
  windowCount : Nat := 0
  /-- Accumulated positive J-cost within the current window. -/
  winJAccum : Nat := 0
  /-- Threshold (ΔJ) for emitting COMMIT events. -/
  commitThreshold : Nat := 1
  /-- History of COMMIT events as (window index, ΔJ). -/
  commitHistory : List (Nat × Nat) := []
  /-- Most recent COMMIT event emitted by the last step, if any. -/
  commitPending : Option Nat := none
  /-- Whether the ConsentDerivative gate is enabled for runtime checks. -/
  consentGate : Bool := false
  /-- Runtime falsifier flags (sticky). -/
  flags : FalsifierFlags := {}
  /-- Sticky falsified bit: once true, remains true. -/
  falsified : Bool := false

/-- Sixteen-op program covering two full eight-beat windows. -/
@[simp] def eightBeatProgram : Array LInstr :=
  kGateProgram ++ kGateProgram

@[simp] def enableConsentGate (s : LState) : LState :=
  { s with consentGate := true }

What this page does not claim

The LNAL VM is not a physical computer; it is a formal model. The progress and preservation theorems do not establish that any particular program halts in finite time. The eight-beat program is a model, not a proof that the framework's derived cycle must be eight ticks.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/LNAL/VM.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: