Lnal Vm Progress

The progress guarantee

The Recognition Science framework includes a small virtual machine, a formal model of a computer that runs programs one instruction at a time. Its state records the current instruction pointer, a breath counter, and a set of working registers. The machine's step function takes a program and a state and produces the next state, and the framework's library proves a property called progress: for any program and any state, there exists a next state. In plain terms, the machine can always take a step; no program can ever leave it stuck with no legal move.

The proof is not a hand-waved argument. It is a theorem in the machine-checked library of formal theorems, with the declaration progress in the VM file. The theorem relies on a companion result, lStep_as_rel, which shows that the step function really does produce a state related to the previous one by the machine's transition relation. Together they establish that the transition relation is total: from every state, at least one successor exists. The machine also satisfies a separate preservation property, preservation_breath, which guarantees that the breath counter stays below its period of 1024 after every step.

What the progress theorem does not claim is equally important. It does not say that every program terminates. A machine can always take a step, but it may run forever, cycling through states indefinitely. Progress is a liveness property about the availability of a next move, not a termination guarantee. The theorem also does not say that the machine's execution is meaningful in any broader sense; it only says that the formal step relation is nonempty at every state. The framework's larger claims about recognition and cost functions are separate results, not consequences of this small machine's progress property.

/-- 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⟩

/-- Functional step embeds into the relational step. -/
@[simp] theorem lStep_as_rel (P : LProgram) (s : LState) :
    LStepRel P s (lStep P s) := LStepRel.step 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
--------------------------------------------------------------------------------

What this page does not claim

The progress theorem does not guarantee that any program terminates; it only ensures every state has a successor. The theorem does not establish any physical or recognition-theoretic meaning for the machine's execution. The progress property is specific to this small virtual machine and does not by itself imply the framework's larger results about cost or dimensions.

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: