ForcedIntegersCert
plain-language theorem explainer
A certificate packaging that logic-naturals embed into the integers as a unital ring homomorphism, that every integer is a difference of two such images, and that negation fixes a difference exactly on the diagonal. Anyone citing the forced integer layer of the δ paper uses this bundle. It is a pure structure definition: fields name the algebraic and geometric obligations, with no proof body.
Claim. A certificate consists of a map $e$ from logic-naturals into $\mathbb{Z}$ with $e(0)=0$, $e(1)=1$, $e(a+b)=e(a)+e(b)$, $e(a\cdot b)=e(a)\cdot e(b)$, and $e$ injective; every $z\in\mathbb{Z}$ equals $e(a)-e(b)$ for some logic-naturals $a,b$; and $e(a)-e(b)=-(e(a)-e(b))$ if and only if $a=b$.
background
Logic-naturals are the two-constructor inductive type forced by the Law of Logic: an identity (zero-cost, multiplicative unit of the orbit) and a step (one further iteration of a generator). Upstream, the orbit embedding sends logic-naturals into the positive reals by iterating a generator value from 1, and is a multiplicative homomorphism for addition of logic-naturals, injective onto the discrete orbit ${1,\gamma,\gamma^2,\ldots}$.
The present module lifts that story from the multiplicative (ratio) layer to an additive integer layer. A companion map toInt (from IntegersFromLogic) is the intended concrete embedding into $\mathbb{Z}$. The certificate records exactly the algebraic and comparison properties the δ paper attributes to that integer layer: unital ring homomorphism, surjectivity of differences, and the diagonal characterization of fixed points of negation on differences.
Local setting is UniversalForcing: once the semiring of forced arithmetic is in hand, one packages the integer extension as a single certificate object rather than a scattered list of lemmas.
proof idea
No proof body: this is a structure definition. Each field is a named obligation (embedding, preservation of $0,1,+ ,\times$, injectivity, surjectivity of differences, and the negation-diagonal biconditional). Downstream, forcedIntegersCert_holds fills the fields by pointing at the concrete toInt map and its already-proved lemmas (toInt_zero, toInt_one, toInt_add, toInt_mul, and the remaining sibling facts on injectivity, nonnegativity, and difference geometry).
why it matters
This certificate is the integer-layer counterpart of the forced-semiring packaging: it makes the δ paper's claim that the integer layer is forced, canonical, and the additive mirror of the ratio layer's comparison geometry into a single checkable object. The sole direct consumer is forcedIntegersCert_holds, which asserts that the certificate is inhabited by the concrete toInt embedding.
In the broader Recognition forcing chain, once logic-naturals and their orbit embedding exist, integers arise as formal differences with a diagonal negation law. That supplies the additive skeleton on which later Hamiltonian and cost-projector constructions sit. The structure does not itself invoke T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$), but it is the arithmetic substrate those geometric forcings presuppose when they talk about integer ranks, rungs, and signed defects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.