CanonicalForcingCert
plain-language theorem explainer
Packages canonicity of arithmetic forcing: between any two strict logic realizations there is a unique Peano equivalence preserving zero and successor. Foundation workers cite it when arguing that forced arithmetic is intrinsic, not a representational choice. As a certificate structure it only records the four obligations; the companion instance discharges them.
Claim. A canonicity certificate asserts that for every pair of strict logic realizations $R,S$ there exists an equivalence $F_{R,S}$ between their forced Peano carriers such that $F_{R,S}(0_R)=0_S$, $F_{R,S}(Sx)=S(F_{R,S}x)$, and any function preserving zero and successor equals $F_{R,S}$.
background
In the universal-forcing layer, a strict logic realization carries a derived lightweight realization from which forced arithmetic is extracted: arith R is the Peano structure on that realization (zero, successor, carrier). The module sits on top of StrictRealization and ArithmeticOf, and asks whether two such forced arithmetics are related by more than a mere bijection of sets.
The intended answer is initiality of Peano arithmetic: any two models linked by zero-and-successor-preserving maps are uniquely isomorphic. Upstream, universal_forcing and its zero/step/uniqueness lemmas already build that map between strict realizations; the present structure is the named bundle of those four properties.
Related canonicity language appears elsewhere in the foundation (e.g. two-valued type canonicity), but here the content is specifically Peano initiality for forced arithmetic, not Boolean constructors.
proof idea
No proof body: this is a structure definition (certificate interface). The four fields are pure obligations: existence of a carrier equivalence for every pair of strict realizations, preservation of zero, preservation of successor, and uniqueness among all zero/successor-preserving functions. Discharge is deferred to the companion instance canonicalForcingCert_holds, which fills each field by the corresponding universal_forcing* lemma on strict realizations.
why it matters
This is the named claim that forcing is canonical rather than representational: forced arithmetic does not depend on which strict realization one started from, up to a unique Peano isomorphism. The sole direct consumer is canonicalForcingCert_holds, whose doc-comment states that the canonicity certificate holds and wires the four fields to universal_forcing, universal_forcing_map_zero, universal_forcing_map_step, and universal_forcing_unique.
In the Recognition Science foundation this closes the uniqueness half of the universal-forcing story: once arithmetic is forced from logic, the forced object is unique. That uniqueness underwrites later claims that physical structure extracted from the arithmetic (octave timing, ladder rungs) is not an artifact of a presentation. It does not itself invoke T5–T8 or the J-cost equation; it is pure logical canonicity upstream of those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.