Foundation Primitive Recognition Calculus Real Null Setoid Real Null Setoid Cond

The conditional certificate

In mathematics, a setoid is a set equipped with an equivalence relation, a way of declaring certain distinct objects to be the same. The declaration real_null_setoid_conditional_certificate is a formal, machine-checked certificate within the Recognition Science framework. It records a precise conditional statement: if a certain analytic property, called the J-cost triangle modulus, is proved, then the framework can construct its real-number carrier as a setoid by quotienting Cauchy sequences under a null-distance relation. The certificate proves this implication, not the analytic property itself.

The certificate is structured as a chain of implications. It shows that the triangle modulus, which says that for any positive tolerance there is a smaller positive tolerance such that two small legs force the composed leg below the original tolerance, is sufficient to prove transitivity of the null-distance relation. From transitivity, the framework derives that the relation is an equivalence, and hence a setoid. The final carrier, PRCRealNull, is then defined as the quotient of Cauchy sequences by this equivalence. This is the standard construction of real numbers as equivalence classes of rational Cauchy sequences, adapted to the framework's cost-based distance.

The certificate is labeled with the strength tag traceClosure, meaning the final quotient still lives under a trace-closure condition. The open obligation is analytic, not a new primitive: no new axioms or definitions are needed beyond proving the triangle modulus. The certificate itself is a theorem in the machine-checked library, with no unproved assumptions. It is a conditional closure, not an unconditional construction of the real numbers.

What the certificate does not claim is equally important. It does not prove the triangle modulus; that remains an open target. It does not assert that the null-distance relation is transitive on its own; it only shows that the triangle modulus would imply transitivity. It does not claim that the quotient carrier is complete or that it satisfies the usual real-number axioms; those are separate steps. The certificate is a precise bookkeeping device: it isolates the exact remaining analytic work and proves that no further structural or definitional choices are needed once that work is done.

/-- Build Order step 9 conditional closure: no quotient mechanics remain once
the local J-cost triangle modulus is proved. -/
theorem real_null_setoid_conditional_certificate :
    PRCRealNullSetoidConditionalCertificate where
  triangle_modulus_target := rfl
  transitive_from_triangle := PRCNullDistanceTransitiveTarget_of_triangle_modulus
  setoid_from_transitive := PRCNullDistanceSetoidTarget_of_transitive
  setoid_from_triangle := PRCNullDistanceSetoidTarget_of_triangle_modulus
  quotient_from_transitive := by
    intro htrans
    exact ⟨PRCRealNull.ofRat htrans 0⟩
  rat_embedding_from_transitive := by
    intro htrans
    exact ⟨PRCRealNull.ofRat htrans⟩
  strength_tag := rfl

/-- 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)

/-- 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

What this page does not claim

The certificate does not prove the triangle modulus itself. The certificate does not assert the null-distance relation is transitive without the triangle modulus. The certificate does not establish completeness or the usual real-number axioms for the quotient carrier.

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: