pith. machine review for the scientific record. sign in
def definition def or abbrev high

radius

show as:
view Lean formalization →

The definition fixes the neighborhood radius at 1 for the one-dimensional cellular automaton that evaluates SAT instances via local rules. Researchers modeling P vs NP through Recognition Science gadgets would cite this constant when building neighborhoods of three cells. The assignment is a direct constant with no further computation or lemmas.

claimThe neighborhood radius satisfies $r = 1$.

background

The Cellular Automata module constructs local gadgets for SAT evaluation inside the Recognition Science framework. It employs a 1D automaton inspired by Rule 110, with each gadget required to be local, deterministic, and reversible for ledger compatibility. The Neighborhood structure holds three CellState values (left, center, right) extracted from the tape at position i, as defined in the sibling structure at line 58.

proof idea

Direct definition that assigns the constant 1. No lemmas or tactics are invoked; the value is supplied verbatim to fix the interaction range for extractNeighborhood and localRule.

why it matters in Recognition Science

This constant sets the locality scale for all CA gadgets that feed the O(n^{1/3} log n) SAT evaluation bound stated in the module. It is referenced by downstream results including normalizedRadius, fr_valence_one, and lower_z_more_remaining in AtomicRadii, which rely on the same radius parameter for shell and valence calculations. The choice aligns with the eight-tick octave (T7) and spatial dimension D=3 landmarks by keeping the neighborhood minimal while preserving reversibility.

scope and limits

formal statement (Lean)

  55def radius : ℕ := 1

proof body

Definition body.

  56
  57/-- Local neighborhood: cells at positions i-1, i, i+1 -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.