forcingFn_succ
plain-language theorem explainer
The universal forcing map between two strict Law-of-Logic realizations intertwines successor: map after succ equals succ after map. Anyone building the forced semiring structure on LogicNat cites this as the inductive step. Proof is a one-line wrapper of the canonical step-intertwining lemma for the universal forcing equivalence.
Claim. For any two strict Law-of-Logic realizations $R$ and $S$, and any logic-natural $n$, the universal forcing map $F_{R,S}:\mathrm{LogicNat}\to\mathrm{LogicNat}$ satisfies $F_{R,S}(\mathrm{succ}\, n)=\mathrm{succ}\, F_{R,S}(n)$.
background
LogicNat is the natural-number type forced by the Law of Logic: two constructors, identity (zero-cost multiplicative unit of the orbit) and step (one more generator iteration). Successor is definitionally step. The structure mirrors the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive-real subset closed under multiplication by $\gamma$ and containing 1.
A strict Law-of-Logic realization supplies only native law data (carrier, cost, zero-cost, compare, compose), with no externally supplied orbit. The universal forcing map between two such realizations is the unique structure-preserving map of their Peano carriers; on the forced carriers it is presented as a self-map of LogicNat.
Upstream, the canonical forcing theorem already states that this equivalence intertwines each realization's Peano step with the other's. The present lemma is that fact rewritten in the ForcedSemiring presentation.
proof idea
One-line term wrapper: apply the upstream theorem that the strict universal-forcing equivalence intertwines $R$'s step with $S$'s step, specialized to the LogicNat presentation of the forced carriers. No extra algebra; the equality is definitionally that map_step property.
why it matters
This is the successor half of the inductive package that makes the forcing map a semiring homomorphism on LogicNat. Downstream, preservation of addition, multiplication, and one are all proved by feeding zero-preservation together with this successor lemma into generic map-preserves lemmas.
In the Recognition foundation stack, unique forced arithmetic is the bridge from the Law of Logic to the later forcing chain (T0–T8). Without successor intertwining, the ForcedSemiring certificate and uniqueness of the forcing map cannot close. The lemma itself is local bookkeeping, but it is the step that turns the abstract initial-object lift into concrete Peano-homomorphism facts used by the rest of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.