Lnal Opcodes Listen Mode

ListenMode

In the Recognition Science framework, a ledger (a discrete record of events) is manipulated by a small set of eight primitive operations called opcodes. One of these, LISTEN, is the operation that observes the state of a token or register. The declaration ListenMode defines the two possible behaviors that LISTEN can carry out: noop, meaning the instruction performs no state change and only observes, and vectorReset, meaning the instruction resets the vector state as part of the observation.

This is a definitional choice, not a derived theorem. The declaration establishes the vocabulary for how the LISTEN opcode can be annotated, alongside other argument types like token actions or balance modes. It does not specify when a program should use one mode over the other, nor does it define what a vector is or how a reset is performed. Those semantics live elsewhere in the framework, if they are defined at all.

In Recognition Science, the framework models computation through these opcodes, and ListenMode is one small piece of that model. It distinguishes observation from vector reset behavior, giving the instruction set a way to express both passive reading and active state clearing. The declaration itself is a structural fact about the instruction set: it names the two modes and makes them part of the formal language of the macrocore ISA.

What ListenMode does not claim is just as important. It does not claim that observation is passive in any physical sense, nor that vector resets are required for correctness. It is a type definition, not a theorem about how recognition must work. The framework's larger claims about forced cost functions and derived constants do not rest on this declaration; ListenMode is a building block, not a proof.

/-- Listen modes distinguish observation from vector reset behaviour. -/
inductive ListenMode
| noop
| vectorReset

What this page does not claim

ListenMode does not define the meaning of observation or vector state. ListenMode does not imply that observation is physically passive. ListenMode is not a theorem about recognition cost or the forcing chain.

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: