intRel_symm
plain-language theorem explainer
Symmetry of the Grothendieck equivalence on pairs of logic-native naturals is established. Researchers assembling the integer type via completion in the Recognition foundation cite it to verify the setoid axioms. The proof is a one-line term wrapper that invokes equality symmetry after introducing the pairs and hypothesis.
Claim. For all pairs $p=(a,b)$ and $q=(c,d)$ of logic-natural numbers, if $a + d = c + b$ then $c + b = a + d$.
background
The module constructs integers from logic-native naturals. LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one iteration of the generator), forming the smallest orbit closed under multiplication by the generator and containing 1. The relation on pairs holds precisely when the crossed sums are equal, encoding formal differences for the Grothendieck construction.
proof idea
The proof is a term-mode one-liner. It introduces the pairs and the hypothesis that the crossed sums are equal, rewrites the goal to the swapped equality, and applies symmetry of equality.
why it matters
The result supplies one of the three setoid axioms required for the quotient that yields the logic-native integers. The downstream setoid instance directly invokes this symmetry together with reflexivity and transitivity. In the Recognition framework it forms part of the foundation layer that precedes the phi-ladder and the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.