toIntCore_respects
plain-language theorem explainer
The theorem shows that the core difference map from pairs of logic naturals to integers is invariant under the equivalence that defines LogicInt. Foundation researchers cite it when constructing the integer recovery map from the quotient. The proof reduces the equivalence hypothesis a + d = c + b to an equality of natural sums via toNat_add, casts to Int, and concludes by linear arithmetic.
Claim. If logic naturals satisfy $a + d = c + b$, then the core map applied to the pair $(a, b)$ equals the core map applied to $(c, d)$, where the core map sends each pair to the integer difference of the iteration counts recovered by toNat.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step, representing the orbit forced by the Law of Logic. The function toNat recovers the iteration count as a standard natural number. LogicInt is the quotient of LogicNat × LogicNat by the equivalence (a, b) ~ (c, d) precisely when a + d = c + b, the Grothendieck completion under addition. The core map toIntCore sends a pair (a, b) to (toNat a : Int) − (toNat b : Int). This theorem establishes that toIntCore descends to the quotient. It relies on the upstream result toNat_add, which states that toNat preserves addition.
proof idea
The proof intros the pairs ⟨a, b⟩ and ⟨c, d⟩ together with the equivalence h : a + d = c + b. It applies congrArg toNat to obtain an equality in Nat, rewrites both sides using toNat_add, casts the resulting equality to Int, and finishes with linarith to equate the two differences.
why it matters
This well-definedness result justifies the definition of the recovery map toInt : LogicInt → Int via Quotient.lift toIntCore toIntCore_respects. It completes the embedding of logic-derived integers into standard integers inside the arithmetic foundation. The parent construction toInt depends directly on it. The step supports later framework elements such as the phi-ladder and the eight-tick octave by supplying a coherent integer structure from the logic naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.