Lnal Registers I32 Range

The 32-bit bound

In computing, a signed 32-bit integer is a whole number that can be positive, negative, or zero, and it is stored in 32 bits of memory. The range it can represent is from −2,147,483,648 to 2,147,483,647. The Recognition Science declaration I32Range, a machine-checked definition in the framework's library, captures this exact boundary: a value x is in range when −2^31 < x < 2^31. It is a closed-form predicate, a precise logical test that any integer either passes or fails.

The context for this bound is the LNAL register block, a set of data structures that hold the execution state of a Recognition Science virtual machine. The main block, Reg6, stores six fields: a log-frequency index, a curvature index, a parity bit, a time-bin index, a transverse mode index, and an entanglement phase. A second block, Aux5, holds five more fields, including a rolling neighbor sum and an active token count. Each of these integer fields is intended to stay within the signed 32-bit range, enforced by compile-time static checks and clamping helpers in the virtual machine.

The declaration itself is modest. It defines the range, and it defines two predicates, Reg6.inI32 and Aux5.inI32, which state that all the integer fields in each block lie within that range. A combined predicate, WellFormed, requires both blocks to be in range and also requires a parity invariant to hold: the parity of the sigma and phiE fields, when combined, must equal the phaseLock boolean. The zero values for both register blocks are also defined, with every integer field set to zero and every boolean field set to false.

In Recognition Science, this declaration is a piece of engineering, not a law of physics. It does not derive the 32-bit range from the forcing chain that produces constants like the golden ratio. It does not claim that any physical quantity must be representable in 32 bits. It does not even prove that the virtual machine's operations will always keep values in range; that is the job of the clamping helpers and static checks the declaration refers to. What I32Range establishes is a clear, checkable contract: here is what it means for a register field to be valid, and here is how that validity is expressed in the formal language.

What the declaration changes is practical. By defining the bound once, the framework gives every tool that reads or writes these registers a single, machine-checked reference for what counts as a legal value. A compiler pass, a simulator, or a proof about the virtual machine can all rely on the same predicate. That is the payoff: one formal definition, used everywhere, so that a value that fits the contract in one place fits it in all places.

The definition does not say anything about what the fields mean. The log-frequency index, the curvature index, and the rest are given names and types, but their physical or mathematical interpretation is left to other documents, such as the LNAL-Register-Mapping.tex schema. The declaration only fixes the bounds within which those meanings are allowed to operate.

/-- Closed form predicate for i32-style range: −2^31 < x < 2^31. -/
def I32Range (x : Int) : Prop := (-i32Bound < x) ∧ (x < i32Bound)

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

What this page does not claim

This declaration does not derive the 32-bit range from the framework's forcing chain of theorems. This declaration does not prove that virtual machine operations will always keep values within the 32-bit range. This declaration does not assign physical meaning to the register fields.

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: