Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Product Continuity Prcjcost Dista

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Real Product Continuity Prcjcost Dista

A machine-checked proof establishes that a specific distance function in the framework's ledger is continuous under multiplication, a key step toward building real numbers from recognition events.

Verify this page

The continuity target

A ledger, a discrete record of events, needs a way to measure how far apart two entries are. The Recognition Science framework defines such a distance function, called the cost distance, for its primitive recognition calculus. The declaration PRCJCostDistanceMulBoundedContinuityTarget_proved is a theorem in the framework's machine-checked library of formal theorems. It proves that this cost distance is continuous with respect to multiplication: if two pairs of entries are each close together, then the products of those pairs are also close together.

Continuity here means a precise, quantitative statement. The theorem shows that for any positive bound M and any desired closeness rho, there exists a smaller closeness eta such that whenever the differences between a and a', and between b and b', are each less than eta (and a', b are bounded by M), then the difference between the products a*b and a'*b' is less than rho. In plainer terms, small changes in the inputs to multiplication produce small changes in the output. This is a standard property of multiplication on real numbers, and the theorem establishes it for the framework's own cost distance.

The proof works by chaining together several lemmas. It first shows that the cost distance display function can be made arbitrarily small by making the square of the underlying difference small (PRCJCostDistanceIncrementDisplay_lt_of_sq_lt), and conversely that a small display value implies a small square (PRCJCostDistance_sq_lt_of_display_lt_delta). It then combines these with a bound on the product of two small differences (product_factor_sq_lt) to arrive at the final product continuity statement (rational_product_increment_sq_lt). The certificate structure PRCRealProductContinuityCertificate bundles this continuity result with closure and congruence properties for multiplication, and the theorem prc_real_product_continuity_certificate constructs that certificate.

What this theorem does not claim is broader. It does not claim that the cost distance is continuous under addition, nor that multiplication is commutative or associative. It does not construct the real numbers themselves; it only certifies one property needed for such a construction. The theorem is a stepping stone within the framework's program, not the program's completion.

THEOREM PRCJCostDistanceMulBoundedContinuityTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealProductContinuity.lean
PRCJCostDistanceMulBoundedContinuityTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealProductContinuity.lean:155 
theorem PRCJCostDistanceMulBoundedContinuityTarget_proved :
    PRCJCostDistanceMulBoundedContinuityTarget := by
  intro eps B heps hB
  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
  let four : PRCRat := two * two
  let rho : PRCRat := eps * (((1 : PRCRat) + eps)⁻¹)
  let K : PRCRat := (1 : PRCRat) + (B * B)
  let eta : PRCRat := rho * ((four * K)⁻¹)
  let delta : PRCRat := (eta * eta) * ((four * ((1 : PRCRat) + eta))⁻¹)
  have heps_pos : (0 : ℚ) < eps.toRat :=
    (PRCRat.positive_iff_toRat_pos eps).mp heps
  have hB_pos : (0 : ℚ) < B.toRat :=
    (PRCRat.positive_iff_toRat_pos B).mp hB
  have htwo : two.toRat = (2 : ℚ) := by
    dsimp [two]
    change (PRCRat.add PRCRat.one PRCRat.one).toRat = (2 : ℚ)
    rw [PRCRat.toRat_add]
    norm_num [PRCRat.one_toRat]
  have hfour : four.toRat = (4 : ℚ) := by
    dsimp [four]
    change (PRCRat.mul two two).toRat = (4 : ℚ)
    rw [PRCRat.toRat_mul]
    norm_num [htwo]
  have h_one_add_eps :
      (((1 : PRCRat) + eps).toRat) = 1 + eps.toRat := by
    change (PRCRat.add PRCRat.one eps).toRat = 1 + eps.toRat
    rw [PRCRat.toRat_add, PRCRat.one_toRat]
  have hK : K.toRat = 1 + B.toRat * B.toRat := by
    dsimp [K]
    change (PRCRat.add PRCRat.one (PRCRat.mul B B)).toRat =
      1 + B.toRat * B.toRat
    rw [PRCRat.toRat_add, PRCRat.one_toRat, PRCRat.toRat_mul]
  have hK_pos : (0 : ℚ) < K.toRat := by
    rw [hK]
    nlinarith [mul_self_nonneg B.toRat]
  have hrho : rho.toRat = eps.toRat / (1 + eps.toRat) := by
    dsimp [rho]
    simp [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_add,
      PRCRat.one_toRat]
    ring
  have hrho_pos : (0 : ℚ) < rho.toRat := by
    rw [hrho]
    positivity
  have hrho_lt_one : rho.toRat < 1 := by
    rw [hrho]
    field_simp [ne_of_gt (by positivity : (0 : ℚ) < 1 + eps.toRat)]
    nlinarith
  have hrho_sq_half_lt_eps : rho.toRat * rho.toRat / 2 < eps.toRat := by
    have hrho_lt_eps : rho.toRat < eps.toRat := by
      rw [hrho]
      field_simp [ne_of_gt (by positivity : (0 : ℚ) < 1 + eps.toRat)]
      nlinarith
    nlinarith [hrho_pos, hrho_lt_one, hrho_lt_eps]
  have heta : eta.toRat = rho.toRat / (4 * K.toRat) := by
    dsimp [eta]
    rw [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_mul, hfour]
    ring
  have heta_pos : (0 : ℚ) < eta.toRat := by
    rw [heta]
    positivity
  have heta_lt_one : eta.toRat < 1 := by
    rw [heta]
    have hden_pos : (0 : ℚ) < 4 * K.toRat := by positivity
    field_simp [ne_of_gt hden_pos]
    have hK_gt_zero : 0 < 4 * K.toRat := by positivity
    nlinarith [hrho_lt_one, hrho_pos, hK_pos]
  have h_one_add_eta :
      (((1 : PRCRat) + eta).toRat) = 1 + eta.toRat := by
    change (PRCRat.add PRCRat.one eta).toRat = 1 + eta.toRat
    rw [PRCRat.toRat_add, PRCRat.one_toRat]
  have hdelta :
      delta.toRat = eta.toRat * eta.toRat / (4 * (1 + eta.toRat)) := by
    dsimp [delta]
    simp [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_add,
      PRCRat.one_toRat, hfour]
    have hden_pos : (0 : ℚ) < 4 * (1 + eta.toRat) := by positivity
    field_simp [ne_of_gt hden_pos]
  have hdelta_pos_rat : (0 : ℚ) < delta.toRat := by
    rw [hdelta]
    positivity
  have hdelta_pos : PRCRat.positive delta := by
    rw [PRCRat.positive_iff_toRat_pos]
    exact hdelta_pos_rat
  refine ⟨delta, hdelta_pos, ?_⟩
  intro a a' b b' ha ha' hb hb' haa hbb
  have ha'_sq : a'.toRat * a'.toRat < B.toRat * B.toRat :=
    PRCRat.InBound_sq_lt hB ha'
  have hb_sq : b.toRat * b.toRat < B.toRat * B.toRat :=
    PRCRat.InBound_sq_lt hB hb
  have haa_rat : PRCJCostDistanceIncrementDisplay (a.toRat - a'.toRat) < delta.toRat := by
    rw [PRCRat.lt_iff_toRat_lt] at haa
    rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment] at haa
    exact haa
  have hbb_rat : PRCJCostDistanceIncrementDisplay (b.toRat - b'.toRat) < delta.toRat := by
    rw [PRCRat.lt_iff_toRat_lt] at hbb
    rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment] at hbb
    exact hbb
  have hda_sq : (a.toRat - a'.toRat) * (a.toRat - a'.toRat) < eta.toRat :=
    PRCJCostDistance_sq_lt_of_display_lt_delta
      (t := a.toRat - a'.toRat) (eta := eta.toRat) (delta := delta.toRat)
      heta_pos hdelta_pos_rat (by rw [hdelta]) haa_rat
  have hdb_sq : (b.toRat - b'.toRat) * (b.toRat - b'.toRat) < eta.toRat :=
    PRCJCostDistance_sq_lt_of_display_lt_delta
      (t := b.toRat - b'.toRat) (eta := eta.toRat) (delta := delta.toRat)
      heta_pos hdelta_pos_rat (by rw [hdelta]) hbb_rat
  have hprod_sq :
      ((a * b).toRat - (a' * b').toRat) *
          ((a * b).toRat - (a' * b').toRat) < rho.toRat := by
    simp [PRCRat.toRat_mul]
    exact rational_product_increment_sq_lt
      (a := a.toRat) (a' := a'.toRat) (b := b.toRat) (b' := b'.toRat)
      (M := B.toRat) (eta := eta.toRat) (rho := rho.toRat)
      hB_pos hrho_pos (by rw [heta, hK]) ha'_sq hb_sq hda_sq hdb_sq
  rw [PRCRat.lt_iff_toRat_lt]
  rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment]
  exact PRCJCostDistanceIncrementDisplay_lt_of_sq_lt
    (t := (a * b).toRat - (a' * b').toRat)
    (eta := rho.toRat) (eps := eps.toRat)
    hrho_pos hrho_lt_one hprod_sq hrho_sq_half_lt_eps
THEOREM rational_product_increment_sq_lt · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealProductContinuity.lean
rational_product_increment_sq_lt · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealProductContinuity.lean:120 
private theorem rational_product_increment_sq_lt
    {a a' b b' M eta rho : ℚ}
    (hM_pos : 0 < M) (hrho_pos : 0 < rho)
    (heta_eq : eta = rho / (4 * (1 + M * M)))
    (ha' : a' * a' < M * M)
    (hb : b * b < M * M)
    (hda : (a - a') * (a - a') < eta)
    (hdb : (b - b') * (b - b') < eta) :
    (a * b - a' * b') * (a * b - a' * b') < rho := by
  let u : ℚ := (a - a') * b
  let v : ℚ := a' * (b - b')
  have hu : u * u < eta * (M * M) := by
    simpa [u] using product_factor_sq_lt
      (da := a - a') (b := b) (eta := eta) (M := M)
      hda hb hM_pos
  have hv : v * v < eta * (M * M) := by
    simpa [v, mul_comm, mul_left_comm, mul_assoc] using product_factor_sq_lt
      (da := b - b') (b := a') (eta := eta) (M := M)
      hdb ha' hM_pos
  have hsum_le : (u + v) * (u + v) ≤ 2 * (u * u) + 2 * (v * v) := by
    nlinarith [mul_self_nonneg (u - v)]
  have hsum_lt : (u + v) * (u + v) < 4 * eta * (M * M) := by
    nlinarith
  have hscale : 4 * eta * (M * M) < rho := by
    rw [heta_eq]
    have hden_pos : (0 : ℚ) < 4 * (1 + M * M) := by positivity
    field_simp [ne_of_gt hden_pos]
    have hM_sq_pos : 0 < M * M := mul_pos hM_pos hM_pos
    nlinarith
  have hidentity : a * b - a' * b' = u + v := by
    dsimp [u, v]
    ring
  rw [hidentity]
  exact lt_trans hsum_lt hscale
THEOREM prc_real_product_continuity_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealProductContinuity.lean
prc_real_product_continuity_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealProductContinuity.lean:282 
theorem prc_real_product_continuity_certificate :
    PRCRealProductContinuityCertificate where
  product_continuity := PRCJCostDistanceMulBoundedContinuityTarget_proved
  mul_closure :=
    PRCRealMulClosureTarget_of_bounded_continuity
      PRCCauchySeqEventuallyBoundedTarget_proved
      PRCJCostDistanceMulBoundedContinuityTarget_proved
  mul_congruence :=
    PRCRealMulCongruenceTarget_of_bounded_continuity
      PRCCauchySeqEventuallyBoundedTarget_proved
      PRCJCostDistanceMulBoundedContinuityTarget_proved
  mul_operation := by
    exact ⟨PRCRealNullClosed.mulOf
      (PRCRealMulClosureTarget_of_bounded_continuity
        PRCCauchySeqEventuallyBoundedTarget_proved
        PRCJCostDistanceMulBoundedContinuityTarget_proved)
      (PRCRealMulCongruenceTarget_of_bounded_continuity
        PRCCauchySeqEventuallyBoundedTarget_proved
        PRCJCostDistanceMulBoundedContinuityTarget_proved)⟩

What this page does not claim

The theorem does not prove continuity under addition. The theorem does not construct the real numbers. The theorem does not establish commutativity or associativity of multiplication.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND