UniversalForcingCert
plain-language theorem explainer
Certificate packaging Universal Forcing: arithmetic forced from any Law-of-Logic realization is an initial Peano algebra, equivalent to the reference naturals, and canonically equivalent across realizations. Foundation authors cite it when wiring the T4–T5 bridge and the inhabited certificate value. Pure structure definition; fields are discharged by existing initiality and orbit-equivalence theorems.
Claim. A Universal Forcing certificate is a record asserting four claims: (1) for any two Law-of-Logic realizations $R,S$, the Peano carriers of their forced arithmetic objects are equivalent; (2) for every realization $R$, that carrier is equivalent to the reference naturals forced by the Law of Logic; (3) every forced arithmetic object satisfies the Peano surface (zero $\neq$ successor, injective successor, induction); (4) arithmetic extracted from any comparison operator on positive reals that satisfies the laws of logic is equivalent, on Peano carriers, to the arithmetic of an arbitrary realization.
background
UniversalForcing states the first formal Universal Forcing theorem: any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects, because those objects are initial Peano algebras.
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity element, and a step/generator; the invariant target is not the ambient carrier but the arithmetic object extracted from identity/step data. ArithmeticOf R packages that object as a Peano algebra together with an initiality witness. The Peano surface records the classical axioms: zero is never a successor, successor is injective, and induction holds on the carrier.
The reference type is LogicNat, the two-constructor inductive forced by the Law of Logic: identity (zero-cost multiplicative unit) and step (one generator iteration), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. Comparison operators on positive reals that satisfy the Aristotelian laws plus scale invariance and non-triviality yield realizations via the positive-ratio construction; the certificate demands that their forced arithmetic match every other realization up to equivalence.
proof idea
No proof body: this is a structure (record type) whose four fields are propositions. Inhabitation is separate. The companion value universalForcingCert fills the fields from existing initiality theorems: invariant and to_reference reduce to composing each realization's orbit equivalence with LogicNat (and its inverse); peano and the continuous positive-ratio clause are likewise discharged by the arithmetic-extraction and surface lemmas already in the ArithmeticOf / LogicRealization stack. One-line field assignments, not a new argument.
why it matters
This is the named packaging of Universal Forcing in the foundation layer: arithmetic is forced uniquely (up to canonical equivalence) from the Law of Logic, independent of which admissible realization one starts from. Downstream, universalForcingCert inhabits the record, and t4_to_t5_cost_bridge_holds in the Unified Forcing Chain consumes the T4 realization bridge packaging. That chain step is the formal bridge toward T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$), though the honesty note on the T4→T5 arrow records that T5 cost uniqueness is proved from CostUniqueness and law-of-logic-forces-jcost and does not logically depend on deleting T−1..T4. The certificate still anchors the claim that forced arithmetic is realization-invariant before cost uniqueness and the later forcing landmarks (phi, eight-tick octave, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.