Foundation Primitive Recognition Calculus Real Order Congruence Prcjcost Distanc

The distance guarantee

The declaration PRCJCostDistance_abs_diff_lt_of_lt_order_delta is a theorem in the machine-checked library of formal theorems that underpins Recognition Science. It establishes a continuity property: if the recognition cost between two events is small, then the underlying values of those events must be close. In plain terms, the cost function cannot hide a large difference between two events behind a tiny cost value. The theorem states that for any positive tolerance gamma, if the cost is below a threshold delta that depends on gamma, then the absolute difference between the two values is strictly less than gamma.

The theorem's precise statement is: for positive rational numbers gamma and delta, if delta is at most (gamma^4) / (4 * (1 + gamma^2)) and the cost PRCJCostDistance a b is less than delta, then -gamma < a - b and a - b < gamma. The proof uses a helper lemma that bounds the square of the difference, then takes square roots. The key point is that the threshold delta is explicit and computable from gamma, not merely asserted to exist. This is a stronger result than a generic continuity statement because it gives a concrete modulus of continuity.

The theorem belongs to a broader development that constructs the real numbers from a primitive recognition calculus. The library also proves that the order relation on these constructed reals is congruent under null equivalence, meaning that if two Cauchy sequences differ by a null sequence, they are ordered the same way. The distance theorem is a separate, more local result about the cost function itself, not about the order structure. It does not claim that the cost function is a metric in the usual sense, nor that it satisfies the triangle inequality, nor that it is symmetric in the sense that PRCJCostDistance a b equals PRCJCostDistance b a for all a and b.

What the theorem does not claim is equally important. It does not assert that the cost function is continuous everywhere in the sense of a full topological space; the statement is only about the specific PRCRat type and the specific cost function. It does not claim that the bound is sharp, only that it holds. It does not claim that the cost function is differentiable or has any particular smoothness property. The theorem is a local, quantitative statement about how small cost implies closeness of values, which is a foundational step for building a calculus of recognition events.

In the framework's own account, this result is one of the pieces that lets the constructed reals behave like ordinary real numbers for the purpose of analysis. It shows that the cost function respects the underlying order and difference structure in a controlled way. A reader who wants to know whether two recognized events are close can use this theorem to convert a cost bound into a difference bound, with an explicit formula for the required threshold.

theorem PRCJCostDistance_abs_diff_lt_of_lt_order_delta
    {a b gamma delta : PRCRat}
    (hgamma : PRCRat.positive gamma)
    (hdelta_pos : PRCRat.positive delta)
    (hdelta_le :
      delta.toRat ≤
        (gamma.toRat * gamma.toRat) * (gamma.toRat * gamma.toRat) /
          (4 * (1 + gamma.toRat * gamma.toRat)))
    (hsmall : PRCRat.lt (PRCJCostDistance a b) delta) :
    -gamma.toRat < a.toRat - b.toRat ∧
      a.toRat - b.toRat < gamma.toRat := by
  let eta : PRCRat := gamma * gamma
  have heta : PRCRat.positive eta := by
    rw [PRCRat.positive_iff_toRat_pos]
    have hgamma_pos : 0 < gamma.toRat :=
      (PRCRat.positive_iff_toRat_pos gamma).mp hgamma
    simp [eta, PRCRat.toRat_mul]
    nlinarith
  have heta_toRat : eta.toRat = gamma.toRat * gamma.toRat := by
    simp [eta, PRCRat.toRat_mul]
  have hsq :
      (a.toRat - b.toRat) * (a.toRat - b.toRat) <
        gamma.toRat * gamma.toRat := by
    have hcore := PRCJCostDistance_sq_diff_lt_of_lt_modulus
      (a := a) (b := b) (eta := eta) (delta := delta)
      heta hdelta_pos (by simpa [heta_toRat] using hdelta_le) hsmall
    simpa [heta_toRat] using hcore
  exact rat_sq_lt_sq_bounds
    ((PRCRat.positive_iff_toRat_pos gamma).mp hgamma) hsq

theorem PRCJCostDistance_abs_diff_lt_of_lt_order_delta
    {a b gamma delta : PRCRat}
    (hgamma : PRCRat.positive gamma)
    (hdelta_pos : PRCRat.positive delta)
    (hdelta_le :
      delta.toRat ≤
        (gamma.toRat * gamma.toRat) * (gamma.toRat * gamma.toRat) /
          (4 * (1 + gamma.toRat * gamma.toRat)))
    (hsmall : PRCRat.lt (PRCJCostDistance a b) delta) :
    -gamma.toRat < a.toRat - b.toRat ∧
      a.toRat - b.toRat < gamma.toRat := by
  let eta : PRCRat := gamma * gamma
  have heta : PRCRat.positive eta := by
    rw [PRCRat.positive_iff_toRat_pos]
    have hgamma_pos : 0 < gamma.toRat :=
      (PRCRat.positive_iff_toRat_pos gamma).mp hgamma
    simp [eta, PRCRat.toRat_mul]
    nlinarith
  have heta_toRat : eta.toRat = gamma.toRat * gamma.toRat := by
    simp [eta, PRCRat.toRat_mul]
  have hsq :
      (a.toRat - b.toRat) * (a.toRat - b.toRat) <
        gamma.toRat * gamma.toRat := by
    have hcore := PRCJCostDistance_sq_diff_lt_of_lt_modulus
      (a := a) (b := b) (eta := eta) (delta := delta)
      heta hdelta_pos (by simpa [heta_toRat] using hdelta_le) hsmall
    simpa [heta_toRat] using hcore
  exact rat_sq_lt_sq_bounds
    ((PRCRat.positive_iff_toRat_pos gamma).mp hgamma) hsq

private theorem rat_sq_lt_sq_bounds {x gamma : ℚ}
    (hgamma : 0 < gamma) (hsq : x * x < gamma * gamma) :
    -gamma < x ∧ x < gamma := by
  constructor
  · by_contra hnot
    have hxle : x ≤ -gamma := by linarith
    have hnonneg : 0 ≤ -x - gamma := by linarith
    have hprod : 0 ≤ (-x - gamma) * (-x + gamma) := by
      have hright : 0 ≤ -x + gamma := by linarith
      exact mul_nonneg hnonneg hright
    nlinarith
  · by_contra hnot
    have hxge : gamma ≤ x := by linarith
    have hnonneg : 0 ≤ x - gamma := by linarith
    have hprod : 0 ≤ (x - gamma) * (x + gamma) := by
      have hright : 0 ≤ x + gamma := by linarith
      exact mul_nonneg hnonneg hright
    nlinarith

What this page does not claim

The cost function is a metric in the usual sense, satisfying symmetry and the triangle inequality. The theorem gives a sharp bound on the difference in terms of the cost. The cost function is differentiable or has any smoothness property beyond this continuity.

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