Lnal Registers Well Formed

The well-formed register

A register is a fixed-size box of integer fields that a machine keeps while it runs. The Recognition Science declaration WellFormed defines what it means for such a box to be in a legal state. It is a definition, not a theorem: it names the conditions that make a state acceptable, and it does not by itself prove that any state exists or that the machine reaches one.

The definition applies to a pair of structures. The first, Reg6, holds six fields: a log-frequency index, a curvature index, a parity bit, a time-bin index, a transverse mode index, and a boolean entanglement phase. The second, Aux5, holds five auxiliary fields: a neighbor sum, a token count, a hydration proxy, a phase-locked flag, and a reserved slot. WellFormed checks three things about the pair. First, every integer field in both structures lies strictly between minus 2^31 and 2^31, the signed 32-bit range. Second, the parity bit and the entanglement phase, taken together, match the phase-locked flag: the sum of the parity bit and the boolean phase, reduced modulo 2, equals the phase-locked flag as 0 or 1. Third, the token count is expected to be 0 or 1, though the definition itself only states the range bound and the parity rule.

The declaration is deliberately narrow. It does not say how the fields get their values, what the neighbor sum means, or what the hydration proxy measures. Those meanings live in comments as domain-defined; the formal definition only pins down the arithmetic shape. It also does not assert that a well-formed state is reachable from any starting point, nor that the machine's operations preserve well-formedness. Those would be separate theorems, and none appear in the pack.

What the definition does give is a precise target for later proofs. If a program wants to show that its execution never leaves a legal state, it can prove that every transition maps a WellFormed pair to another WellFormed pair. The declaration supplies the predicate; the reachability and preservation arguments remain open work.

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

/-- Signed 32-bit bound used for simple clamping. -/
@[simp] def i32Bound : Int := 2147483648  -- 2^31

/-- Parity coupling: (sigma + phiE) mod 2 equals phaseLock. -/
def parityInvariant (r : Reg6) (a : Aux5) : Prop :=
  ((parity2 r.sigma + bit r.phiE) % 2) = bit a.phaseLock

What this page does not claim

WellFormed does not prove that any register state is reachable. WellFormed does not define the meaning of the neighbor sum or hydration proxy fields. WellFormed does not assert that the machine's operations preserve well-formedness.

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: