Foundation Primitive Recognition Calculus Grow Eta Completion M0a Cross Eq Of Eq

The embedding is faithful

The declaration crossEq_of_equiv_eta is a theorem inside the Recognition Science framework's machine-checked library of formal theorems. It concerns the framework's construction of real numbers from sequences of rationals, a construction that follows the same broad strategy as the classical real numbers: take a set of objects, declare two of them equivalent when they are close enough in a precise sense, and form the collection of equivalence classes. The theorem states that the map sending each rational to its constant sequence is injective, meaning it never identifies two different rationals. In plain language: if two constant sequences are considered equivalent, then the original rationals must already have been equal.

The proof is short because the construction is careful. The framework represents a rational number by a pair of integers, its numerator and denominator. Two rationals are declared equal when a certain cross-difference, the integer a.num * b.den - b.num * a.den, equals zero. The theorem crossEq_of_equiv_eta shows that if the constant sequences built from two rationals are equivalent under the real-number equivalence relation, then that cross-difference is zero. The equivalence relation on sequences is defined by a bound on the cross-difference of the sequence terms as the index grows, and for constant sequences the bound collapses to the condition that the cross-difference itself is zero.

The consequence is that the embedding of the framework's rational numbers into its real numbers is faithful: it preserves distinctness. This is a basic sanity property for any construction of the reals, and the framework's library proves it holds. The theorem does not claim that every real number arises this way, nor does it establish any property of the real numbers beyond this injectivity. It is a small but necessary step in building a usable number system inside the framework.

/-- The Archimedean step: if the constant sequences at `q` and `r` are
equivalent (their fixed difference is below every `1/(k+1)`), then `q` and `r`
are cross-equal. Instantiate the tolerance at `k = den q * den r`; then
`c * (k+1) ≤ k` forces `c = 0`. Choice-free. -/
theorem crossEq_of_equiv_eta {q r : RatioOrbit}
    (h : equiv (eta q) (eta r)) : RatioOrbit.crossEq q r := by
  set k := q.den.toNat * r.den.toNat with hk
  obtain ⟨N, hN⟩ := h k
  have hbound := hN N (Nat.le_refl N)
  rw [eta_seq q N, eta_seq r N, ← hk] at hbound
  -- hbound : |crossDiff q r| * (k+1) ≤ k, so |crossDiff q r| = 0.
  have hzero : (crossDiff q r).natAbs = 0 := by
    by_contra hne
    have hone : 1 ≤ (crossDiff q r).natAbs := Nat.pos_of_ne_zero hne
    have : k + 1 ≤ (crossDiff q r).natAbs * (k + 1) := by
      calc k + 1 = 1 * (k + 1) := (Nat.one_mul _).symm
        _ ≤ (crossDiff q r).natAbs * (k + 1) := Nat.mul_le_mul_right (k + 1) hone
    exact absurd (le_trans this hbound) (by omega)
  have hcd : crossDiff q r = 0 := Int.natAbs_eq_zero.mp hzero
  rw [RatioOrbit.crossEq_iff_toIntCross]
  unfold crossDiff at hcd
  omega

/-- The cross-difference: the integer numerator of `a - b`,
i.e., `a.num * b.den - b.num * a.den`. This avoids the ℚ display entirely. -/
def crossDiff (a b : RatioOrbit) : ℤ :=
  a.num.toInt * (b.den.toNat : ℤ) - b.num.toInt * (a.den.toNat : ℤ)

What this page does not claim

The theorem does not prove that every real number is the image of some rational. The theorem does not establish any algebraic or order properties of the real numbers. The theorem does not claim that the equivalence relation on sequences is the same as equality of limits in the classical sense.

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: