universalForcingCert
plain-language theorem explainer
Packages the Universal Forcing theorem as a single certificate: arithmetic extracted from any Law-of-Logic realization is Peano, canonically equivalent to LogicNat, and therefore equivalent across realizations. Foundation workers cite it when they need one object that records invariance, reference equivalence, and the Peano surface together. The body just wires existing orbit equivalences and the peano-surface lemma into the certificate fields.
Claim. There is a Universal Forcing certificate: for any two Law-of-Logic realizations $R,S$, the Peano carriers of their extracted arithmetic are canonically equivalent; for every realization $R$ that carrier is equivalent to $\mathrm{LogicNat}$; every such arithmetic has the Peano surface; and the same reference equivalence holds for continuous positive-ratio realizations.
background
UniversalForcing states that any two Law-of-Logic realizations force the same arithmetic surface, because those surfaces are initial Peano algebras. A realization supplies a free orbit under a generator; arithmeticOf extracts the Peano algebra on that orbit.
LogicNat is the reference natural-number type forced by the Law of Logic: constructors identity (zero-cost multiplicative unit) and step (one generator iterate), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. Each realization carries an equivalence orbitEquivLogicNat from its orbit to this reference type.
The certificate structure records four obligations: pairwise carrier equivalence, equivalence to LogicNat, the Peano surface on every extracted arithmetic, and the continuous positive-ratio variant of the invariance. The Peano-surface obligation is already proved by peano_surface, which reduces to ArithmeticOf.extracted_peanoSurface.
proof idea
Definitional inhabitant of the certificate structure; each field is a short term or one-line proof.
invariant: rewrite the goal as orbit equivalence, then composeR.orbitEquivLogicNatwith the inverse ofS.orbitEquivLogicNat.to_reference: same rewrite, discharge byR.orbitEquivLogicNatalone.peano: apply the existing theorempeano_surface R.continuous_positive_ratio_invariant: rewrite toLogicNat ≃ S.Orbitand useS.orbitEquivLogicNat.symm.
No new arithmetic is constructed; the certificate only assembles initiality already present on realizations.
why it matters
This is the paper-upgrade packaging of Universal Forcing inside the Foundation layer: one named object that says forced arithmetic is unique up to canonical equivalence. The module doc frames it as the first formal statement of that theorem. Downstream the certificate is the natural handle for any argument that must transport Peano structure, induction, or arithmetic identities between realizations without re-proving initiality.
In the broader Recognition chain it sits under the logic-to-arithmetic bridge that precedes cost uniqueness (T5), the golden fixed point (T6), and the eight-tick / dimension forcing steps. It does not itself force $\varphi$ or $J$; it guarantees that whatever arithmetic those later steps use is the same object no matter which admissible realization one started from. No used_by edges are recorded yet, so the certificate is presently a terminal packaging point rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.