Foundation Primitive Recognition Calculus Real Null Setoid

The null-distance quotient

A setoid is a set equipped with an equivalence relation, a way of declaring some elements to be the same before you form a quotient. The classical real numbers arise this way: Cauchy sequences of rationals are declared equivalent when their differences tend to zero, and the real numbers are the resulting equivalence classes. This construction builds the same structure inside Recognition Science, where the notion of "distance" comes not from a metric but from a cost function.

The cost function J(x) = (x + 1/x)/2 - 1 measures the price of recognizing one value as another. From it, the framework defines a distance between rationals, and then a distance between Cauchy sequences of rationals. Two sequences are null-equivalent when this distance can be made arbitrarily small. The construction proves that this relation is reflexive and symmetric directly from the definitions. The missing piece is transitivity: if a is close to b and b is close to c, then a must be close to c. That requires a triangle-inequality-like property for the cost distance.

The construction isolates exactly what is needed. It defines a target statement, the triangle modulus: for every positive tolerance epsilon there exists a smaller positive delta such that two legs each shorter than delta force the composed leg shorter than epsilon. The construction then proves that this analytic property is sufficient. Given the triangle modulus, transitivity follows, the null-equivalence becomes a full equivalence relation, and the quotient PRCRealNull is a well-defined setoid. Rationals embed into it as constant sequences. The construction is conditional on the triangle modulus, which remains an open analytic obligation.

In Recognition Science, this is Build Order step 9. The construction records a conditional certificate: it proves that no quotient mechanics remain once the triangle modulus is proved. The remaining work is analytic, not structural. The framework's library of machine-checked theorems shows that the entire real-number construction reduces to one local inequality about the cost distance. This matters because it pins down where the framework's real numbers come from: not from a postulate about completeness, but from the forced cost function and a single unproved analytic estimate.

/-- A transitivity proof turns `PRCNullEquivalent` into a setoid. -/
def PRCNullDistanceSetoidOfTransitive
    (htrans : PRCNullDistanceTransitiveTarget) : Setoid PRCCauchySeq where
  r := PRCNullEquivalent
  iseqv := by
    constructor
    · exact PRCNullEquivalent.refl
    · intro u v
      exact PRCNullEquivalent.symm
    · intro u v w
      exact htrans u v w

/-- The analytic triangle modulus is sufficient for null-distance
transitivity. All remaining work here is completed-orbit index bookkeeping. -/
theorem PRCNullDistanceTransitiveTarget_of_triangle_modulus
    (htri : PRCJCostDistanceTriangleModulusTarget) :
    PRCNullDistanceTransitiveTarget := by
  intro u v w huv hvw eps heps
  rcases htri eps heps with ⟨delta, hdelta_pos, hdelta⟩
  rcases huv delta hdelta_pos with ⟨Nuv, hNuv⟩
  rcases hvw delta hdelta_pos with ⟨Nvw, hNvw⟩
  refine ⟨max Nuv Nvw, ?_⟩
  intro n hn
  have hn_uv : Nuv ≤ n := le_trans (Nat.le_max_left Nuv Nvw) hn
  have hn_vw : Nvw ≤ n := le_trans (Nat.le_max_right Nuv Nvw) hn
  exact hdelta (u.term n) (v.term n) (w.term n)
    (hNuv n hn_uv) (hNvw n hn_vw)

/-- Conditional final real carrier: once the analytic triangle modulus is
proved, this is the intended PRC real quotient by null distance. -/
def PRCRealNull (htrans : PRCNullDistanceTransitiveTarget) : Type :=
  Quot (PRCNullDistanceSetoidOfTransitive htrans)

/-- The exact setoid target follows from the sharper triangle-modulus target. -/
theorem PRCNullDistanceSetoidTarget_of_triangle_modulus
    (htri : PRCJCostDistanceTriangleModulusTarget) :
    PRCNullDistanceSetoidTarget :=
  PRCNullDistanceSetoidTarget_of_transitive
    (PRCNullDistanceTransitiveTarget_of_triangle_modulus htri)

What this page does not claim

The triangle modulus itself is proved; it remains an open analytic obligation. The null-distance quotient is the classical real numbers; the construction only yields the setoid conditionally. The quotient is complete; completeness is not addressed by this construction.

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/RealNullSetoid.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: