logicNat_interprets_into_lattice
plain-language theorem explainer
Every primitive interface equipped with a base configuration and successor map admits an interpretation of the forced naturals LogicNat into its recognition lattice, sending the identity to the base cell and each successor to the image cell under iterated application of the map. Researchers formalizing arithmetic embeddings in Recognition Science cite this when constructing the pre-spatial quotient from a recognizer. The proof is a one-line term that invokes the auxiliary constructor logicNatToLattice and discharges the two mapping equations by
Claim. For any type $K$ and primitive interface $I$ on $K$, given base element $b$ and step function $s:K→K$, there exists a map $ι:LogicNat→RecognitionLattice(I)$ such that $ι(identity)=cellOf(I,b)$ and $ι(step n)=cellOf(I,s(iteratedCarrier(b,s,n)))$ for all $n$.
background
RecognitionLattice(I) is the quotient of the carrier by the kernel equivalence interfaceSetoid(I), so its elements are indistinguishability classes of configurations under the primitive observer. LogicNat is the inductive type with constructors identity (zero-cost element) and step (one further iteration), mirroring the orbit {1,γ,γ²,…} forced by the Law of Logic. The module shows that any such lattice is the recognition quotient, pre-spatial and carrying finite-resolution neighborhoods inherited from the event codomain Fin n. Upstream, the identity event sits at the J-cost minimum and LogicNat is the smallest subset closed under the generator and containing 1.
proof idea
The proof is a one-line term wrapper: it supplies the pair consisting of the function logicNatToLattice I base step together with the two reflexivity proofs that the identity and successor cases match the required cells.
why it matters
This supplies the logicNat_interpretation field of recognitionLatticeCert, completing the certificate that every primitive interface yields a lattice admitting the universal iteration object. It realizes the module claim that LogicNat interprets into the recognition quotient, linking the forcing chain to the pre-spatial lattice before spatial dimensions or metric structure are derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.