Foundation Primitive Recognition Calculus Grow Eta Completion M0a Cross Diff Swa

The cross-difference swap

A rational number is a ratio of two integers, like 3/4. When two rational numbers are written with explicit numerators and denominators, the difference between them can be expressed as a single integer: the cross-difference. For a = p/q and b = r/s, the cross-difference is p*s - r*q. This integer is zero exactly when the two rationals are equal. The declaration crossDiff_swap proves a basic symmetry: the cross-difference of b minus a is the negative of the cross-difference of a minus b. In symbols, crossDiff b a = -crossDiff a b. This mirrors how ordinary subtraction behaves: 5 - 3 = 2, and 3 - 5 = -2.

This fact is proved in the framework's machine-checked library of formal theorems. It is one small lemma inside a larger construction that builds real numbers from sequences of rationals. The proof itself is a direct algebraic expansion, using the ring structure of integers. It does not depend on any special property of the rationals beyond their arithmetic. The declaration is a theorem, meaning it is a proved statement, not an assumption.

In Recognition Science, this lemma supports the definition of an equivalence relation on sequences of rationals. Two sequences are equivalent when their cross-differences shrink to zero in a controlled way. The swap property is needed to show that this equivalence is symmetric: if sequence s is equivalent to sequence t, then t is equivalent to s. Without the swap, the symmetry proof would fail. The lemma is a technical building block, not a headline result.

What crossDiff_swap does not claim is broader. It does not say anything about the real numbers that the sequences converge to. It does not assert that the cross-difference is a metric or a distance. It does not prove that the equivalence relation is transitive or that the quotient construction works. Those are separate theorems in the same file. The swap is a single algebraic identity, no more and no less.

/-- Antisymmetry of the cross-difference: `crossDiff b a = -crossDiff a b`. -/
theorem crossDiff_swap (a b : RatioOrbit) : crossDiff b a = -crossDiff a b := by
  unfold crossDiff
  ring

/-- Cross-equal rationals have zero cross-difference. -/
theorem crossDiff_of_crossEq (a b : RatioOrbit) (h : RatioOrbit.crossEq a b) :
    crossDiff a b = 0 := by
  rw [RatioOrbit.crossEq_iff_toIntCross] at h
  unfold crossDiff
  omega

/-- `equiv` is symmetric. The cross-difference only flips sign, so its absolute
value and the denominator product are unchanged. Choice-free. -/
theorem equiv_symm {s t : RegularSeq} (h : equiv s t) : equiv t s := by
  intro k
  obtain ⟨N, hN⟩ := h k
  refine ⟨N, ?_⟩
  intro n hn
  have hcd : crossDiff (t.seq n) (s.seq n) = -crossDiff (s.seq n) (t.seq n) :=
    crossDiff_swap (s.seq n) (t.seq n)
  rw [hcd, Int.natAbs_neg, Nat.mul_comm (t.seq n).den.toNat (s.seq n).den.toNat]
  exact hN n hn

What this page does not claim

This lemma does not define a distance or a metric on rationals. It does not prove that the equivalence relation on sequences is transitive. It says nothing about the real numbers that the sequences converge to.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/EtaCompletionM0a.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: