add
plain-language theorem explainer
Addition on LogicInt is defined by lifting componentwise sum on pairs of LogicNat through the quotient. Researchers building the integer ring from logical primitives cite this when assembling the additive monoid. The construction uses Quotient.lift₂ with a well-definedness proof that reduces equivalences to Nat equalities via toNat and toNat_add before applying omega.
Claim. Let $Z_ℓ$ be the quotient of $N_ℓ × N_ℓ$ by the equivalence $(a,b) ∼ (c,d)$ iff $a + d = b + c$. Addition is then $[a,b]_ℓ + [c,d]_ℓ = [a + c, b + d]_ℓ$.
background
LogicInt is the quotient type Quotient (setoid : Setoid (LogicNat × LogicNat)), providing the integers as formal differences of logic naturals. LogicNat is the inductive type generated by identity and step, mirroring the multiplicative orbit {1, γ, γ², ...} in positive reals as described in its doc-comment. The upstream theorem eq_iff_toNat_eq states that an equation in LogicNat holds if and only if it holds under toNat, serving as the bridge to ordinary arithmetic. Similarly, toNat_add recovers that LogicNat addition matches Nat addition. This sits in the IntegersFromLogic module, extending ArithmeticFromLogic to construct the additive group.
proof idea
The definition is a one-line wrapper around Quotient.lift₂ applied to the map (p, q) ↦ mk (p.1 + q.1) (p.2 + q.2). The accompanying proof of well-definedness assumes equivalent pairs via hab and hcd, applies sound to reduce to an equality of sums, then uses eq_iff_toNat_eq together with six invocations of toNat_add to reach a Nat equation. Two auxiliary lemmas extract the crossed sums, after which omega closes the goal.
why it matters
This supplies the addition operation needed to turn LogicInt into an additive monoid, feeding the construction of the full ring structure on integers derived from logic. It advances the foundation layer toward the forcing chain T0-T8 by establishing basic arithmetic before introducing J-uniqueness or the phi fixed point. No downstream uses are yet recorded, leaving open its integration into mass formulas or Berry thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.