Lnal Opcodes Token Action

Token actions

TokenAction is a data type, a definitional choice, in the machine-checked library of formal theorems behind Recognition Science. It defines the two ways a primitive instruction can change a token register, which is a discrete record of a number associated with a token. The first way is delta, which adds a whole number to the current value. The second is set, which replaces the value with a new whole number and can also record a cost for that replacement, a whole number that defaults to zero.

The declaration sits inside the macrocore ISA, a family of eight primitive opcodes: LOCK, BALANCE, FOLD, SEED, BRAID, MERGE, LISTEN, and FLIP. TokenAction is not itself an opcode; it is an argument type that opcodes like FOLD or SEED can carry. The library provides convenience constructors that pair a token action with an opcode, so a program can write a single instruction such as "set this token to 5" or "add 3 to this token". The constructors are named tokenSet and tokenDelta, and they exist to keep instruction construction short and uniform.

What TokenAction does not claim is as important as what it defines. It does not define what a token is, what a ledger is, or how recognition events are recorded. Those concepts belong to other parts of the framework. It does not specify which opcodes may use which actions; that policy lives in the instruction constructors, not in the TokenAction type itself. It does not say what the cost field means physically or economically. The cost is a whole number attached to a set action, and its interpretation is left to the layer above.

The declaration is a vocabulary, not a theorem. It establishes that the language of token manipulation has exactly two primitive verbs, and that both verbs operate on whole numbers. This is a modeling choice: the framework chooses to represent token changes as either an increment or a replacement. Nothing in the declaration forces a particular value, a particular cost, or a particular sequence of actions. The consequence for a reader is that TokenAction gives a precise, minimal grammar for talking about token changes, and any richer behavior must be built from these two moves.

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

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

/-- Convenience constructor for token-setting instructions (seed/spawn/gc). -/
@[simp] def tokenSet (op : Opcode) (value : Int) (cost : Int := 0) : LInstr :=
  { op := op, arg := OpcodeArg.token (TokenAction.set value cost) }

/-- Convenience constructor for token deltas (give/regive style). -/
@[simp] def tokenDelta (op : Opcode) (delta : Int) : LInstr :=
  { op := op, arg := OpcodeArg.token (TokenAction.delta delta) }

What this page does not claim

TokenAction does not define what a token or a ledger is. TokenAction does not specify which opcodes may use which actions. TokenAction does not assign a physical or economic meaning to the cost field.

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: