Lnal Vm Eight Beat Alignment Detail

The eight-beat alignment detail

An eight-beat alignment is a fixed sequence of eight instruction steps that a virtual machine executes in a loop. The sequence is built by running the same four-step gate program twice in a row, so the machine's state after step eight matches the pattern it saw after step four. The definition in the framework's machine-checked library of formal theorems names this loop eightBeatProgram and provides a trace of every machine state the loop passes through, from the initial register settings to the final committed state.

The detail's purpose is bookkeeping, not physics. It records, for each of the eight steps, which of the machine's eight window indices is active, how many windows have rolled over, and whether a commit is pending. It also tracks a running sum that accumulates the perpendicular component of a register, and it checks that this sum increases by exactly that component at every step. These are the ledger facts: a discrete record of events, kept step by step, that the framework uses to describe how recognition cost is spent inside a window.

In Recognition Science, the framework models a recognition event as a cost that a system must pay, and the eight-tick cycle is the framework's derived rhythm for that payment. The eight-beat alignment detail is the machine-level expression of that rhythm: it shows, in executable form, how the framework's abstract cycle maps onto a concrete sequence of register updates and window rolls. What the detail establishes is that this mapping is internally consistent, that the trace is finite, and that the machine always has a next step to take.

What the detail does not claim is that this eight-step loop is the only possible alignment, or that the virtual machine itself is a physical object. The definition is a model, a choice of how to represent the cycle in code, not a proof that nature runs this program. The framework's theorems about the eight-tick cycle live elsewhere; this declaration only fixes the machine's behavior under that choice.

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

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

/-- Enumerated eight-beat vector exposing window/count progression and commit flag. -/
def eightBeatVector : List (Nat × Nat × Nat × Bool) :=
  (List.zip (List.range eightBeatTrace.length) eightBeatTrace).map fun
    | (step, st) => (step, st.winIdx8, st.windowCount, st.commitPending.isSome)

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

What this page does not claim

The eight-beat alignment is the only possible instruction sequence for the framework's cycle. The virtual machine is a physical object whose steps correspond to real-world events. This declaration proves the eight-tick cycle itself; that derivation is a separate theorem.

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: