intRel_refl
Reflexivity of the Grothendieck equivalence on pairs of logic-native naturals holds by direct substitution. Researchers constructing LogicInt via completion of LogicNat cite this to confirm the relation is an equivalence before quotienting. The proof introduces the pair and reduces immediately to reflexivity of equality on the component sum.
claimFor every pair of logic-native natural numbers $p = (a, b)$, the relation defined by $(a, b) ~ (c, d)$ iff $a + d = c + b$ satisfies $(a, b) ~ (a, b)$.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), forming the smallest subset of positive reals closed under multiplication by the generator and containing 1. The relation intRel on pairs encodes the Grothendieck equivalence: $(a, b) ~ (c, d)$ holds precisely when $a + d = c + b$, so that the pair $(a, b)$ represents the formal difference $a - b$. This module extends the arithmetic already derived for LogicNat by completing it to integers under this equivalence.
proof idea
The proof is a short tactic sequence: introduce the arbitrary pair p, unfold the definition of intRel to obtain the goal p.1 + p.2 = p.1 + p.2, and close by reflexivity of equality.
why it matters in Recognition Science
Reflexivity is one of the three properties required to instantiate the Setoid structure on LogicNat × LogicNat, which in turn defines LogicInt as the quotient. This step completes the passage from logic-forced naturals to integers inside the foundation layer, supplying the additive group structure needed for later mass and dimension derivations in the Recognition Science chain.
scope and limits
- Does not prove symmetry or transitivity of intRel.
- Does not construct the quotient type LogicInt itself.
- Applies only to pairs of LogicNat; no extension to other types is shown.
Lean usage
instance setoid : Setoid (LogicNat × LogicNat) := ⟨intRel, intRel_refl, intRel_symm, intRel_trans⟩formal statement (Lean)
45theorem intRel_refl : ∀ p : LogicNat × LogicNat, intRel p p := by
proof body
Term-mode proof.
46 intro p
47 show p.1 + p.2 = p.1 + p.2
48 rfl
49