intRel_symm
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove reflexivity or transitivity of the relation.
- Does not construct the quotient type of logic-native integers.
- Does not connect to the J-cost function or Recognition Composition Law.
- Does not address physical constants or spatial dimensions.
formal statement (Lean)
50theorem intRel_symm : ∀ {p q : LogicNat × LogicNat}, intRel p q → intRel q p := by
proof body
Term-mode proof.
51 intro p q h
52 show q.1 + p.2 = p.1 + q.2
53 exact h.symm
54