logicNatToLattice_step
plain-language theorem explainer
The step lemma equates the lattice image of a successor in LogicNat to the cell of the stepped iterated carrier. Researchers building the recognition quotient from a primitive observer cite this when unfolding the recursive map. The equality is definitional, so the proof is reflexivity.
Claim. Let $I$ be a primitive interface on carrier $K$, $b$ a base point in $K$, and $s:K→K$ a step function. For any logic-natural number $n$, the lattice image of the successor of $n$ equals the cell containing $s$ applied to the $n$-fold iteration of $s$ on $b$.
background
The module constructs the recognition lattice as the quotient of the carrier $K$ by the kernel of the observe map in PrimitiveInterface, where two configurations are equivalent precisely when the finite-valued observer cannot distinguish them. LogicNat is the inductive type with constructors identity (zero-cost element) and step (one more iteration of the generator), mirroring the multiplicative orbit under a generator. The function logicNatToLattice recursively applies cellOf after iterating the step function on the base. Upstream, cellOf is the quotient constructor mk on the interfaceSetoid, and the step parameter is an arbitrary $K→K$ map (distinct from the cellular-automata step that applies a local rule globally).
proof idea
The proof is a term-mode reflexivity on the definition of logicNatToLattice, which matches on the LogicNat.step constructor and returns exactly cellOf I (step (iteratedCarrier base step n)).
why it matters
The lemma supplies the inductive step for interpreting the universal iteration object LogicNat into the pre-spatial recognition lattice, completing the module claim that every primitive interface admits such an interpretation. It realizes the mapping from the forcing-chain iteration structure into lattice cells before metric or spatial structure appears. No downstream uses are recorded, leaving open how the lattice image feeds into later constructions such as the phi-ladder or D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.