Lnal Instr Cost

The instruction cost table

In Recognition Science, a ledger (a discrete record of events) is processed by a small set of primitive instructions. The framework assigns each instruction a cost in dimensionless units, a number that says how much recognition work one execution of that instruction consumes. The cost is not a runtime measurement; it is a definitional choice, fixed by the model of computation.

The instruction set has four opcodes. FOLD, which combines two ledger entries, costs 0 when it folds along direction 0 and 1 otherwise. BRAID and MERGE, which rearrange or combine tokens, each cost a value d taken from their token argument. SEED, which sets a token's cost field, costs exactly the value it writes. Any instruction not matching these patterns costs 0. The full rule is a single function: instrCost maps each instruction to its integer price.

The plain-language content of the framework is a pricing table. It establishes that every instruction has a well-defined cost, that the cost is an integer, and that the cost of SEED is the value it stores. Nothing in the framework proves that these prices are optimal or forced; the theorems about forced costs apply to the recognition cost function J, not to this instruction-level table. The table is the model's choice of how to charge for computation steps.

What this framework changes is the accounting layer of the model. With a fixed price per instruction, any sequence of operations has a definite total cost, and the model can ask which sequences are cheapest. The table is the first place where the abstract idea of recognition cost becomes a concrete, computable number for actual machine steps.

/-- J-cost rate for a primitive instruction (dimensionless units). -/
def instrCost : LInstr → Int
  | ⟨Opcode.FOLD, OpcodeArg.fold dir⟩ => if dir = 0 then 0 else 1
  | ⟨Opcode.FOLD, _⟩ => 1
  | ⟨Opcode.BRAID, OpcodeArg.token (TokenAction.delta d)⟩ => d
  | ⟨Opcode.MERGE, OpcodeArg.token (TokenAction.delta d)⟩ => d
  | ⟨Opcode.SEED, OpcodeArg.token (TokenAction.set _ cost)⟩ => cost
  | _ => 0

/-- J-cost rate for a primitive instruction (dimensionless units). -/
def instrCost : LInstr → Int
  | ⟨Opcode.FOLD, OpcodeArg.fold dir⟩ => if dir = 0 then 0 else 1
  | ⟨Opcode.FOLD, _⟩ => 1
  | ⟨Opcode.BRAID, OpcodeArg.token (TokenAction.delta d)⟩ => d
  | ⟨Opcode.MERGE, OpcodeArg.token (TokenAction.delta d)⟩ => d
  | ⟨Opcode.SEED, OpcodeArg.token (TokenAction.set _ cost)⟩ => cost
  | _ => 0

/-- J-cost rate for a primitive instruction (dimensionless units). -/
def instrCost : LInstr → Int
  | ⟨Opcode.FOLD, OpcodeArg.fold dir⟩ => if dir = 0 then 0 else 1
  | ⟨Opcode.FOLD, _⟩ => 1
  | ⟨Opcode.BRAID, OpcodeArg.token (TokenAction.delta d)⟩ => d
  | ⟨Opcode.MERGE, OpcodeArg.token (TokenAction.delta d)⟩ => d
  | ⟨Opcode.SEED, OpcodeArg.token (TokenAction.set _ cost)⟩ => cost
  | _ => 0

What this page does not claim

This framework does not prove that any instruction cost is forced or optimal. This framework does not define the recognition cost function J itself. This framework does not claim that the integer costs are the only possible pricing scheme.

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