Lnal Registers

The execution state

In Recognition Science, the ledger, a discrete record of events, needs a place to keep its current state while it operates. The LNAL registers are that place: a fixed set of numbered slots, defined in a machine-checked library of formal theorems, that hold the working values of a running process. The design splits the state into a core block of six registers, named Reg6, and an auxiliary block of five, named Aux5.

The six core registers carry the physical meaning of the process. One holds a log-frequency index, a position on a logarithmic scale of frequencies. Another holds a curvature or orbital index. A third holds a parity bit, encoded as a small integer. The remaining three hold a time-bin index, a transverse or mode index, and a boolean entanglement phase. Each slot is an integer, and the whole block is designed to stay within signed 32-bit ranges, enforced by static checks and clamping helpers in the virtual machine.

The five auxiliary registers track execution details rather than physics. They hold a rolling signed neighbor sum, an active token count expected to be 0 or 1, a hydration or free-volume proxy, a phase-locked indicator that is either core or glassy, and one reserved domain-specific slot. Together the two blocks form the complete execution state, and a well-formed state is one where every integer field lies in the signed 32-bit range and a parity coupling holds: the parity of the core's sigma and entanglement phase must match the auxiliary's phase-locked bit.

What this framework establishes is a precise contract for what a valid state is. It defines the zero state, the range predicates, and the well-formedness condition that combines them. This matters because the framework's later theorems about how a process evolves assume the state starts and stays well-formed. The registers are not a claim about physics; they are the vocabulary in which such claims get written.

structure Reg6 where
  /-- ν_φ: log-frequency index (φ-lattice) -/
  nuPhi : Int
  /-- ℓ: curvature / orbital index -/
  ell   : Int
  /-- σ: parity bit encoded as {−1,0,+1} or small integers -/
  sigma : Int
  /-- τ: time-bin index within higher-level domain -/
  tau   : Int
  /-- k_⊥: transverse/mode index -/
  kPerp : Int
  /-- φ_e: entanglement phase (boolean) -/
  phiE  : Bool

structure Aux5 where
  /-- Rolling signed neighbor sum (domain-defined) -/
  neighborSum : Int
  /-- Active token count (0/1 expected by invariants) -/
  tokenCt     : Int
  /-- Hydration/free-volume proxy (domain-defined) -/
  hydrationS  : Int
  /-- Phase-locked indicator (core/glassy) -/
  phaseLock   : Bool
  /-- Reserved domain-specific slot -/
  freeSlot    : Int

/-- Combined well-formedness for a register + auxiliary pair. -/
def WellFormed (r : Reg6) (a : Aux5) : Prop := r.inI32 ∧ a.inI32 ∧ parityInvariant r a

structure Reg6 where
  /-- ν_φ: log-frequency index (φ-lattice) -/
  nuPhi : Int
  /-- ℓ: curvature / orbital index -/
  ell   : Int
  /-- σ: parity bit encoded as {−1,0,+1} or small integers -/
  sigma : Int
  /-- τ: time-bin index within higher-level domain -/
  tau   : Int
  /-- k_⊥: transverse/mode index -/
  kPerp : Int
  /-- φ_e: entanglement phase (boolean) -/
  phiE  : Bool

structure Aux5 where
  /-- Rolling signed neighbor sum (domain-defined) -/
  neighborSum : Int
  /-- Active token count (0/1 expected by invariants) -/
  tokenCt     : Int
  /-- Hydration/free-volume proxy (domain-defined) -/
  hydrationS  : Int
  /-- Phase-locked indicator (core/glassy) -/
  phaseLock   : Bool
  /-- Reserved domain-specific slot -/
  freeSlot    : Int

What this page does not claim

No claim that the register contents correspond to any measured physical quantity. No claim that the parity invariant is derived from the forcing chain; it is a definitional choice. No claim that the reserved freeSlot has a fixed meaning.

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