eq_iff_toInt_eq
The equivalence relating equality of constructed integers to equality of their images under the recovery map serves as the central transfer principle for ring axioms. Foundation researchers establishing algebraic identities from logical primitives cite it to reduce proofs to standard integers. The proof splits the biconditional via constructor, applies direct congruence in one direction, and invokes the round-trip embedding in the converse.
claimLet $a$ and $b$ be elements of the Grothendieck completion of the logic naturals under addition. Then $a = b$ if and only if the image of $a$ under the canonical recovery map to the integers equals the image of $b$ under the same map.
background
LogicInt is defined as the quotient of pairs of logic naturals by the equivalence that identifies $(a,b)$ with $(c,d)$ precisely when $a + d = b + c$, yielding the Grothendieck completion under addition. The recovery map toInt lifts the core difference function $a - b$ to this quotient, while fromInt embeds each standard integer back by placing non-negative values in the first component and negatives in the second. The upstream round-trip result states that fromInt composed with toInt recovers every element of the completion.
proof idea
The term proof opens the biconditional with constructor. The forward direction is immediate from congruence of the recovery map. The converse assumes equality of the images, applies the embedding map to both sides, and rewrites each occurrence via the round-trip identity to obtain equality in the completion.
why it matters in Recognition Science
This equivalence is invoked by every subsequent ring axiom on the constructed integers, including associativity and commutativity of addition and multiplication, each of which rewrites via the transfer and reduces to the ring tactic on standard integers. It thereby transfers the full integer ring structure into the logic-derived foundation, supplying the arithmetic layer required before the J-cost functional and the phi-ladder mass formula can be introduced.
scope and limits
- Does not define addition or multiplication on the constructed integers.
- Does not itself verify the ring axioms.
- Does not extend the transfer to other algebraic structures.
- Does not address decidability or computational extraction.
Lean usage
theorem add_assoc' (a b c : LogicInt) : (a + b) + c = a + (b + c) := by rw [eq_iff_toInt_eq, toInt_add, toInt_add, toInt_add, toInt_add]; ringformal statement (Lean)
360theorem eq_iff_toInt_eq {a b : LogicInt} : a = b ↔ toInt a = toInt b := by
proof body
Term-mode proof.
361 constructor
362 · exact congrArg toInt
363 · intro h
364 have := congrArg fromInt h
365 rw [fromInt_toInt, fromInt_toInt] at this
366 exact this
367
368/-! ## 7. Ring Axioms on `LogicInt`
369
370By transfer through `toInt`, every ring identity on `LogicInt`
371reduces to one on `Int` and is closed by `ring`. -/
372