Lnal Opcodes Opcode Arg

Instruction metadata

In the LNAL instruction set, an opcode is a primitive command, and OpcodeArg is the optional metadata that refines it. The core opcode family has exactly eight primitives: LOCK, BALANCE, FOLD, SEED, BRAID, MERGE, LISTEN, and FLIP. Each instruction is a pair: a primitive opcode plus an argument, where the argument defaults to "none" when no extra information is needed. This mirrors how a load instruction in a conventional processor might take a register operand, except here the arguments are fixed, typed, and few.

The arguments themselves form four small families. A FOLD instruction takes a direction, an integer that says which way to fold. A token argument carries a token action, either a delta (add or subtract an integer) or a set (write a value, with an optional cost). A balance argument selects a mode: window, which resets a neutral window, or cycle, which resets the full cycle. A listen argument selects noop or vectorReset, distinguishing plain observation from a vector reset. These are the only argument shapes; the declaration is an inductive type, which in a machine-checked library means the list is closed and exhaustive by construction.

In Recognition Science, the ledger is a discrete record of events. The argument types exist to annotate primitives with macro-level intent: they say what kind of bookkeeping a command performs, not how the underlying arithmetic is carried out. The convenience constructors in the same file, such as LInstr.fold or LInstr.tokenSet, build full instructions from a short name and an argument, so programs read as intent rather than as raw bit patterns.

What OpcodeArg does not claim is important. It does not define the semantics of any opcode; it only names the metadata shapes. It does not say what FOLD does with its direction, or how BALANCE resets a window; those behaviors live elsewhere, in the execution model. It also does not introduce new primitive operations. The eight opcodes are fixed, and the arguments only refine them. The declaration is a vocabulary, not a program, and it is a definitional choice, not a derived theorem.

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

/-- Opcode arguments annotate primitives with macro-level intent. -/
inductive OpcodeArg
| none
| fold (dir : Int)
| token (action : TokenAction)
| balance (mode : BalanceMode)
| listen (mode : ListenMode)

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

What this page does not claim

This declaration does not define the runtime behavior of any opcode. It does not add new primitives beyond the eight listed. It does not prove any theorem about what the instructions compute.

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: