Lnal Registers Parity Invariant

The parity invariant

In the Recognition Science framework, a computation keeps a discrete record of its own state, a ledger of events that the framework models as a machine with registers. Two of those registers matter here. One, called Reg6, holds six fields describing a recognition event: a frequency index, a curvature index, a parity bit, a time index, a transverse mode index, and an entanglement flag. The other, Aux5, holds five auxiliary values including a phase-lock indicator that says whether the system is in a core or glassy state.

The declaration named parityInvariant establishes a single consistency rule between those two registers. It states that the parity of the sum of the parity bit and the entanglement flag, taken modulo 2, must equal the phase-lock indicator. In plainer terms: if the two parity-related fields in Reg6 have odd total parity, then the phase-lock bit in Aux5 must be 1; if they have even total parity, the phase-lock bit must be 0. The rule is a definition, not a theorem; it defines what it means for a register pair to be well-formed.

The declaration also carries a companion definition, WellFormed, which combines three conditions: all integer fields in both registers lie within signed 32-bit bounds, and the parity invariant holds. This is the framework's way of saying that a register pair is only considered valid when its fields stay in range and its parity bookkeeping agrees. The parity invariant is one of several such consistency checks; it does not by itself describe how the registers change over time, nor does it specify what any particular field means physically.

What the declaration does not claim is just as important. It does not prove that any actual computation satisfies the invariant; it only defines the condition. It does not assign a physical interpretation to the parity bit, the entanglement flag, or the phase-lock indicator; those meanings live in the framework's modeling choices, not in this declaration. And it does not say anything about the golden ratio, the forcing chain, or any of the framework's larger results; this is a local consistency rule for one register pair, not a global law.

/-- 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

/-- 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

/-- 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

The invariant does not prove that any actual computation satisfies it; it only defines the condition. The declaration does not assign physical meanings to the parity bit, entanglement flag, or phase-lock indicator. The parity invariant does not state anything about the golden ratio or the framework's global laws.

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: