Lnal Opcodes

The opcode family

An opcode, short for operation code, is the basic command in a computer's instruction set. The lnal opcodes define a small, fixed family of eight such commands: LOCK, BALANCE, FOLD, SEED, BRAID, MERGE, LISTEN, and FLIP. Each one names a distinct kind of action that can be taken on a ledger, a discrete record of events. The definitions establish the vocabulary for describing these actions in the Recognition Science framework.

The eight opcodes are not arbitrary labels. They correspond to the fundamental operations that the framework's model of recognition requires. LOCK secures a value, BALANCE resets a running total, FOLD changes direction, SEED sets an initial token, BRAID combines two strands, MERGE joins records, LISTEN observes or resets a vector, and FLIP inverts a state. Each opcode can carry an optional argument that specifies its intent. FOLD takes a direction, BALANCE distinguishes between a window reset and a full cycle reset, and LISTEN separates simple observation from a vector reset.

Token actions, the second major piece, describe how primitives manipulate the ledger's token register. Two actions exist: delta, which adds an integer to the current value, and set, which replaces the value outright and can optionally record a cost. Convenience constructors wrap these into single instructions, so that a token-setting instruction for SEED or a token-delta instruction for a give-style operation can be written in one line.

In Recognition Science, the framework models recognition events as operations on a ledger, and the opcode family is the instruction set for those operations. The definitions establish that there are exactly eight primitive command types, that each can be annotated with one of four argument kinds, and that instructions are simply an opcode paired with an optional argument. This is a definitional choice, not a derived theorem: the vocabulary is chosen, and it is not proved that these eight are the only possible commands. What is provided is a fixed, machine-checked language in which the framework's later results about recognition cycles and costs can be stated.

For a reader coming from conventional computer science, the payoff is a concrete picture: the framework's abstract ledger is not a vague metaphor but a precise data structure with a small, complete set of operations. For a reader coming from Recognition Science, the opcodes are the atoms out of which the eight-tick recognition cycle is built. Knowing the instruction set is the first step to understanding what the framework means when it says that recognition has a forced structure.

/-- Core opcode family for the macrocore ISA (8 primitives). -/
inductive Opcode
| LOCK
| BALANCE
| FOLD
| SEED
| BRAID
| MERGE
| LISTEN
| FLIP

/-- Token actions used by primitives that manipulate the ledger/token register. -/
inductive TokenAction
| delta (d : Int)
| set (value : Int) (cost : Int := 0)

/-- Core instruction: primitive opcode plus optional argument metadata. -/
structure LInstr where
  op : Opcode
  arg : OpcodeArg := .none

What this page does not claim

The eight opcodes are proven to be the only possible primitive operations. The module proves any theorem about recognition cycles or costs. The opcodes define a Turing-complete instruction set.

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/Opcodes.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: