intRel_refl
plain-language theorem explainer
Reflexivity of the Grothendieck equivalence on pairs of logic-forced natural numbers holds by direct reduction to equality. Researchers constructing the integers via completion of the logic orbit cite this result to verify the relation is reflexive. The proof introduces an arbitrary pair and discharges the defining equality by the reflexivity tactic.
Claim. Let $N$ be the inductive type of logic-forced natural numbers. Define the relation $sim$ on $N times N$ by $(a,b) sim (c,d)$ if and only if $a + d = c + b$. Then for every pair $p$, one has $p sim p$.
background
LogicNat is the inductive type with constructors identity and step, representing the orbit {1, gamma, gamma squared, ...} as the smallest subset of positive reals closed under multiplication by gamma and containing the multiplicative identity. The relation intRel is the Grothendieck equivalence on pairs: (a, b) ~ (c, d) precisely when a + d = c + b, allowing formal differences a - b. This theorem resides in the module that builds the integers from the arithmetic forced by logic and imports the definition of LogicNat from ArithmeticFromLogic.
proof idea
The proof is a short tactic sequence. It introduces the pair p, states the goal explicitly as the equality of the two component sums, and applies the reflexivity tactic rfl to conclude.
why it matters
This reflexivity supplies one of the three axioms needed for the setoid instance on LogicNat pairs, which is then used to form the quotient type LogicInt as the Grothendieck completion. It fills the reflexive slot in the foundation step that precedes the phi-ladder and the derivation of physical constants such as the fine-structure constant in the Recognition Science framework. The downstream setoid instance directly incorporates this theorem together with symmetry and transitivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.