iteratedCarrier
plain-language theorem explainer
The iteratedCarrier definition supplies the recursive unfolding of LogicNat into an arbitrary carrier type K, starting from a base element and applying a step function at each successor. Researchers constructing interpretations of forced arithmetic into recognition lattices cite this when building the canonical map from the iteration object. The definition proceeds by direct pattern matching on the two constructors of LogicNat.
Claim. The recursive map $f :$ LogicNat $→ K$ defined by $f($identity$) = $base and $f($step $n) = $step$(f(n))$, for given base point base $∈ K$ and successor function step $: K → K$.
background
LogicNat is the inductive type forced by the Law of Logic, with constructors identity (the zero-cost multiplicative identity) and step (one further iteration of the generator), mirroring the orbit {1, γ, γ², …}. The module RecognitionLatticeFromRecognizer constructs the recognition quotient lattice as the quotient of a carrier by the primitive observer's indistinguishability kernel; cells are equivalence classes of configurations that the recognizer cannot distinguish, inheriting finite resolution from the event codomain Fin n. Upstream, ArithmeticFromLogic.LogicNat supplies the iteration object while ArithmeticOf.canonical provides the realization-independent Peano surface.
proof idea
This is the direct recursive definition of the carrier map by pattern matching on LogicNat.identity (returning base) and LogicNat.step n (returning step applied to the recursive call on n).
why it matters
iteratedCarrier is the concrete carrier map used inside logicNatToLattice and logicNat_interprets_into_lattice to realize the canonical interpretation of LogicNat into RecognitionLattice I. It therefore supplies the missing step in the module's claim that every primitive interface admits a LogicNat interpretation into its recognition lattice. The construction sits inside the Recognition Geometry program that converts the structural claim of kernel-equivalence classes into a lattice, linking to the T0-T8 forcing chain via the universal iteration object LogicNat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.