Lnal Registers Reg6

The execution register

Reg6 is a data structure defined in the machine-checked library of formal statements used by Recognition Science. It is a register block, a fixed arrangement of six fields that hold the execution state of a computation in the LNAL virtual machine. The fields are named ν_φ (a log-frequency index), ℓ (a curvature or orbital index), σ (a parity bit), τ (a time-bin index), k_⊥ (a transverse or mode index), and φ_e (an entanglement phase, stored as a boolean). Together they describe the state of a single computational step, not a physical object.

The declaration establishes what a well-formed Reg6 state is. A companion structure, Aux5, holds five auxiliary fields: a rolling neighbor sum, an active token count, a hydration proxy, a phase-locked indicator, and a reserved slot. The key definition is WellFormed, which requires three things. First, all integer fields of both structures must lie within signed 32-bit bounds, meaning each is greater than -2^31 and less than 2^31. Second, the auxiliary fields must satisfy the same bound. Third, a parity invariant must hold: the sum of the parity bit σ and the entanglement phase φ_e, taken modulo 2, must equal the phase-locked indicator in Aux5.

This is a definitional choice, not a result that is proven. The declaration does not claim that any physical system actually occupies a Reg6 state, nor that the parity invariant describes a natural law. It defines a constraint that a computation must satisfy to be considered well-formed. The zero value of Reg6, with all fields set to zero and the boolean false, is also defined as a starting point. The purpose is to give the virtual machine a precise, checkable notion of a valid state.

In Recognition Science, the framework models physical structure as a ledger of recognition events, and this register is a tool for tracking computational state within that model. The declaration is infrastructure: it sets up the vocabulary for describing execution, not a result about the world. Its role is to make later claims precise by fixing what a valid state is, so that any statement about LNAL execution can be made against a clear background.

What Reg6 does not claim is as important as what it does. It does not assert that the six fields correspond to measurable physical quantities, nor that the parity invariant is a law of nature. It does not derive any property of the golden ratio, the fine-structure constant, or any other constant from the framework's forcing chain. It is a definition, tagged as a model, and its only content is the structure it defines.

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

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

@[simp] def zero : Reg6 :=
  { nuPhi := 0, ell := 0, sigma := 0, tau := 0, kPerp := 0, phiE := false }

What this page does not claim

Reg6 does not assert that its fields correspond to measurable physical quantities. The parity invariant is not claimed to be a law of nature. No property of the golden ratio or the fine-structure constant is derived from this declaration.

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: