canonicalForcingCert_holds
plain-language theorem explainer
Packages the universal-forcing theorems into a single canonicity certificate: any two strict logic realizations have a unique Peano-preserving equivalence of forced arithmetic. Cited wherever the framework needs a one-shot witness that arithmetic is forced, not chosen. The body is a pure structure instance wiring four already-proved map/zero/step/uniqueness lemmas.
Claim. There is a canonicity certificate asserting: for every pair of strict logic realizations $R,S$, there exists an equivalence of their forced Peano carriers that sends zero to zero, intertwines the successor maps, and is the unique function with those two properties.
background
Universal forcing says that any two Law-of-Logic realizations induce canonically equivalent forced arithmetic objects. In the strict setting, a realization carries a forced Peano structure (carrier, zero, successor) obtained from the initial-object lift in the arithmetic-of construction.
The certificate structure records four obligations: existence of the carrier equivalence for every pair of strict realizations; preservation of zero; intertwining of successor; and uniqueness of any zero-and-step-preserving map. Upstream, the abstract spine already supplies a universal forcing map as the initial-object equivalence between arithmetic-of objects; the strict variants specialize that map and prove its Peano morphisms and uniqueness from the initial-lift uniqueness law.
Locally this module assembles those strict facts into one named certificate that forcing is canonical rather than representational: the equivalence is determined by zero/step data alone.
proof idea
One-line structure instance. Each field of the certificate is filled by the corresponding strict universal-forcing lemma: existence by the strict universal forcing equivalence; zero preservation by the zero-map theorem; successor intertwining by the step-map theorem; uniqueness by the canonicity theorem that any zero-and-step-preserving function equals the forcing map. No new argument is introduced.
why it matters
Closes the canonicity claim in the Universal Forcing layer: forced arithmetic between strict realizations is unique and structure-preserving, so there is no representational freedom in the Peano data. That is the content of the certificate doc: forcing is canonical, not representational. Downstream consumers (none linked yet in the graph) can cite the single certificate rather than four separate lemmas when discharging "arithmetic is forced" hypotheses in the foundation chain. It sits under the Universal Forcing Meta-Theorem spine and supports the broader Recognition claim that arithmetic structure is forced by the logic realization, not chosen by convention. No open scaffold remains in this packaging step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.