ForcedSemiringCert
plain-language theorem explainer
Certificate that distinction forces the arithmetic semiring, not merely the tower. For any two strict Law-of-Logic realizations the canonical forcing map on logic-naturals is a bijection preserving zero, one, addition and multiplication, and is the unique zero-and-successor-preserving map. Foundation work that cites the forced object (ℕ, 0, 1, +, ×) uses this interface. Pure structure: the inhabitant is assembled from the forcing-function lemmas.
Claim. A forced-semiring certificate supplies, for every pair of strict Law-of-Logic realizations $R,S$, a map $f_{R,S}$ on logic-naturals that is bijective; sends $0\mapsto 0$ and $1\mapsto 1$; preserves addition and multiplication; and is the unique map with $f(0)=0$ and $f(n+1)=f(n)+1$.
background
Logic-naturals are the inductive type forced by the Law of Logic: an identity constructor (zero-cost multiplicative unit) and a step constructor (one more generator iteration), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive-real subset closed under multiplication by $\gamma$ and containing 1. Successor is one application of the generator; the Peano axioms are theorems of that inductive structure, not postulates.
A strict Law-of-Logic realization carries only native law data: a carrier, a cost type with a zero, a comparison map, and composition, with no supplied orbit. Universal forcing compares any two such realizations via a canonical map on the forced naturals.
This module records that the comparison is a full semiring isomorphism of those naturals, not merely a tower correspondence.
proof idea
Structure definition with empty body: it packages seven fields rather than proving them. The fields demand a family of maps on logic-naturals indexed by pairs of strict realizations; bijectivity of each map; preservation of zero, one, addition, and multiplication; and uniqueness among maps that fix zero and commute with successor. The separate holding definition fills every field from the forcing function and the already-proved lemmas on that function (bijectivity, zero/one/add/mul laws, uniqueness).
why it matters
The holding definition in the same module is the sole direct consumer: it wires the forcing function and its preservation lemmas into one certificate object. That upgrades tower-level forcing to full arithmetic: the forced object is canonically the semiring $(\mathbb{N},0,1,+,\times)$. In the Recognition foundation this sits inside universal forcing from the Law of Logic, supporting the claim that arithmetic is forced by distinction rather than assumed. Downstream proofs that need a single handle on "the unique zero/step map between realizations is a semiring isomorphism" cite the holding instance. It does not itself touch J-uniqueness, $\phi$, the eight-tick octave, or $D=3$; those live elsewhere in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.