Lnal Vm Preservation Breath

The breath bound

A virtual machine is a simulated computer with its own rules for memory, registers, and instruction execution. The one described here tracks a recognition cost, a number that measures how much work a step of computation consumes, and it divides time into windows of 1024 steps. The machine keeps a running count called the breath, which resets to zero when a window rolls over. The declaration preservation_breath proves a simple guarantee: after any single instruction executes, the breath count is still inside its window, meaning it is always less than 1024.

This is not a statement about what a program does. It does not say a program halts, computes a particular answer, or stays within any other resource limit. It says only that the breath counter, which the machine increments each step and wraps around at the window boundary, never lands outside the allowed range after a step. The proof works by a direct arithmetic argument: the counter is defined to increase by one and then take the remainder after division by 1024, so the result is always in the range from 0 to 1023. The theorem is checked in a machine-checked library of formal theorems, meaning a computer program verified the logic step by step.

The guarantee matters because the breath counter is part of a budget. The machine's design gives each window a finite allowance of recognition cost, and the breath tracks how much of that allowance has been spent. If the counter could overflow, the budget would be meaningless. The theorem closes that hole for a single step, and because it holds for every state and every program, it holds for every step of every run. It is a local invariant: one step at a time, the machine stays within its accounting frame.

In Recognition Science, this theorem is a small piece of a larger structure. The framework models reality as a ledger, a discrete record of events, and this virtual machine is a concrete implementation of that idea. The breath bound is not a claim about physics. It does not say the universe actually runs on this machine, nor that real computation must obey this exact window size. It is a formal result about a defined object: if you build a machine with a breath counter that wraps at 1024, then that counter stays in range. The consequence for a reader is practical: the budget mechanism is sound, and the machine's accounting never silently breaks.

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

@[simp] def lFetch (P : LProgram) (ip : Nat) : LInstr := P ip
@[simp] def lNextIP (s : LState) : Nat := s.ip + 1
@[simp] def lBumpBreath (s : LState) : Nat := (s.breath + 1) % breathPeriod

What this page does not claim

The theorem does not claim any program halts or produces a correct result. It does not claim the virtual machine models real physical computation. It does not claim the breath counter measures anything beyond its own defined arithmetic.

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: