logicNatToLattice
plain-language theorem explainer
This definition supplies the canonical map sending each element of the logically forced naturals into the quotient lattice of configurations indistinguishable under a given primitive observer. It is cited when constructing arithmetic interpretations inside recognition structures or when proving that LogicNat acts on equivalence classes. The map is realized directly by sending each iterated point to its cell in the kernel quotient.
Claim. Let $I$ be a primitive interface on carrier $K$, with base point $b$ and successor map $s:K→K$. The function from the inductive type of logically forced naturals (generated by an identity element and a successor constructor) to the recognition lattice of $I$ sends each such natural $n$ to the equivalence class of the $n$-fold iterate of $s$ applied to $b$.
background
A primitive interface on carrier $K$ consists of a positive integer $n$ together with an observation map from $K$ to the finite set with $n$ elements; its kernel is the equivalence relation of configurations that produce identical observations. The recognition lattice is the quotient of $K$ by this kernel, so its points are the indistinguishable classes. LogicNat is the smallest inductive type containing an identity element and closed under a successor constructor, mirroring the orbit generated by repeated multiplication by the forcing generator.
proof idea
One-line definition that composes the iterated-carrier function with the cellOf quotient map: each LogicNat element is sent to the lattice cell containing the corresponding carrier iterate.
why it matters
The definition is invoked directly by the theorems logicNat_interprets_into_lattice, logicNatToLattice_zero and logicNatToLattice_step, which establish that every primitive interface admits a LogicNat interpretation. It realizes the module's claim that kernel-equivalence classes form the first recognition lattice and supplies the concrete map needed to embed the universal iteration object into that pre-spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.