Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcjcost Distance Increment Triangle

ARTICLE 5 claims 5 theorems

Foundation Primitive Recognition Calculus Prcjcost Distance Increment Triangle

A small formula about a cost increment turns out to be the hinge that lets Recognition Science build real numbers from scratch.

Verify this page

The distance increment

A distance increment is the change in a cost function when a recognition event moves a small step. In Recognition Science, the ledger (a discrete record of events) assigns a cost to each step, and the increment is the difference between the cost at the new position and the cost at the old one. The central formula states that for a rational step size t, the displayed increment equals (t²)² / (2(1 + t²)). This is a proved theorem, not a definition: the expression follows from the underlying cost structure.

The formula matters because it is small. As t approaches zero, the increment shrinks like t⁴, which is fast enough to make a certain kind of comparison work. Two complementary estimates are proved. First, if t² is small, then the increment is small. Second, if the increment is small, then t² is small. Together they show that the increment and the step size carry exactly the same information about smallness, a property mathematicians call an equivalence of moduli.

That equivalence is the load-bearing piece. The framework wants to identify two ledgers as representing the same real number when their distance is zero. The triangle inequality, the rule that a direct distance is never longer than a path through an intermediate point, is what makes this identification well behaved. The increment estimates prove the triangle inequality for the null-distance relation, which means the relation is transitive: if A is null-distance to B, and B is null-distance to C, then A is null-distance to C. Transitivity is the hard part of showing that the relation is an equivalence, and the module closes it with the explicit rational estimates.

With transitivity proved, the framework can quotient the ledgers by null distance and obtain a carrier for the real numbers. The module packages this as a certificate: a single structure containing the increment formula, the triangle modulus, transitivity, and the existence of the quotient carrier. The certificate is proved in the machine-checked library of formal theorems, so the entire chain, from the increment formula to the real-number carrier, is verified by the computer.

What this establishes in plain language is that the framework's path to real numbers is internally consistent. The cost increment is not an arbitrary choice; its smallness behavior is forced by the cost structure, and that behavior is exactly what is needed to make the null-distance quotient work. The module is a bridge: it connects the primitive cost calculus to the construction of the real numbers, and it does so with a proof that the computer has checked end to end.

THEOREM PRCJCostDistanceIncrementDisplay_formula · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean
PRCJCostDistanceIncrementDisplay_formula · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean:19 
theorem PRCJCostDistanceIncrementDisplay_formula (t : ℚ) :
    PRCJCostDistanceIncrementDisplay t =
      ((t * t) * (t * t)) / (2 * (1 + t * t)) := by
  unfold PRCJCostDistanceIncrementDisplay PRCJCostDistanceRatDisplay
  have hg_pos : (0 : ℚ) < 1 + t * t := by
    nlinarith [mul_self_nonneg t]
  have hg_ne : (1 + t * t : ℚ) ≠ 0 := ne_of_gt hg_pos
  field_simp [hg_ne]
  ring
THEOREM increment_display_lt_of_sq_lt · sq_lt_of_display_lt_delta · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean
increment_display_lt_of_sq_lt · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean:29 
private theorem increment_display_lt_of_sq_lt
    {t eta eps : ℚ} (heta_pos : 0 < eta) (heta_lt_one : eta < 1)
    (hsq : t * t < eta) (heta_sq_half_lt_eps : eta * eta / 2 < eps) :
    PRCJCostDistanceIncrementDisplay t < eps := by
  rw [PRCJCostDistanceIncrementDisplay_formula]
  have hs_nonneg : (0 : ℚ) ≤ t * t := mul_self_nonneg t
  have hden_pos : (0 : ℚ) < 2 * (1 + t * t) := by positivity
  have hden_ne : (2 * (1 + t * t) : ℚ) ≠ 0 := ne_of_gt hden_pos
  have hs_lt_one : t * t < 1 := lt_trans hsq heta_lt_one
  have hnum_lt : (t * t) * (t * t) < eta * eta := by nlinarith
  have hfrac_le : ((t * t) * (t * t)) / (2 * (1 + t * t)) ≤
      ((t * t) * (t * t)) / 2 := by
    have hden_ge_two : (2 : ℚ) ≤ 2 * (1 + t * t) := by nlinarith
    have hnum_nonneg : (0 : ℚ) ≤ (t * t) * (t * t) :=
      mul_nonneg hs_nonneg hs_nonneg
    exact div_le_div_of_nonneg_left hnum_nonneg (by norm_num) hden_ge_two
  have hnum_half_lt : ((t * t) * (t * t)) / 2 < eta * eta / 2 := by
    nlinarith
  exact lt_of_le_of_lt hfrac_le (lt_trans hnum_half_lt heta_sq_half_lt_eps)
sq_lt_of_display_lt_delta · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean:49 
private theorem sq_lt_of_display_lt_delta
    {t eta delta : ℚ} (heta_pos : 0 < eta) (_hdelta_pos : 0 < delta)
    (hdelta_le : delta ≤ eta * eta / (4 * (1 + eta)))
    (hsmall : PRCJCostDistanceIncrementDisplay t < delta) :
    t * t < eta := by
  by_contra hnot
  have hge : eta ≤ t * t := by nlinarith
  rw [PRCJCostDistanceIncrementDisplay_formula] at hsmall
  have hs_nonneg : (0 : ℚ) ≤ t * t := mul_self_nonneg t
  have hs_pos : (0 : ℚ) < t * t := lt_of_lt_of_le heta_pos hge
  have hden_s_pos : (0 : ℚ) < 2 * (1 + t * t) := by positivity
  have hden_eta_pos : (0 : ℚ) < 4 * (1 + eta) := by positivity
  have hmono :
      eta * eta / (4 * (1 + eta)) ≤
        ((t * t) * (t * t)) / (2 * (1 + t * t)) := by
    let s : ℚ := t * t
    have hs_ge : eta ≤ s := by simpa [s] using hge
    have hs_nonneg' : (0 : ℚ) ≤ s := by simpa [s] using hs_nonneg
    have hs_den_pos : (0 : ℚ) < 2 * (1 + s) := by positivity
    have h_eta_den_two_pos : (0 : ℚ) < 2 * (1 + eta) := by positivity
    have h_eta_den_four_pos : (0 : ℚ) < 4 * (1 + eta) := by positivity
    have hhalf :
        eta * eta / (4 * (1 + eta)) ≤
          eta * eta / (2 * (1 + eta)) := by
      have hnum_nonneg : (0 : ℚ) ≤ eta * eta := by nlinarith
      have hden_le : 2 * (1 + eta) ≤ 4 * (1 + eta) := by nlinarith
      exact div_le_div_of_nonneg_left hnum_nonneg h_eta_den_two_pos hden_le
    have hmon :
        eta * eta / (2 * (1 + eta)) ≤
          (s * s) / (2 * (1 + s)) := by
      have hdiff_nonneg :
          0 ≤ s * s * (1 + eta) - eta * eta * (1 + s) := by
        have hleft : 0 ≤ s - eta := by nlinarith
        have heta_nonneg : 0 ≤ eta := le_of_lt heta_pos
        have hright : 0 ≤ s + eta + s * eta := by
          nlinarith [mul_nonneg hs_nonneg' heta_nonneg]
        have hprod : 0 ≤ (s - eta) * (s + eta + s * eta) :=
          mul_nonneg hleft hright
        nlinarith
      field_simp [ne_of_gt hs_den_pos, ne_of_gt h_eta_den_two_pos]
      nlinarith [hdiff_nonneg]
    exact le_trans hhalf (by simpa [s] using hmon)
  exact not_lt_of_ge (le_trans hdelta_le hmono) hsmall
THEOREM PRCJCostDistanceTriangleModulusTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean
PRCJCostDistanceTriangleModulusTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean:207 
/-- The PRC triangle modulus is now closed by the explicit rational increment
estimate. -/
theorem PRCJCostDistanceTriangleModulusTarget_proved :
    PRCJCostDistanceTriangleModulusTarget :=
  PRCJCostDistanceTriangleModulusTarget_of_verifier
    PRCJCostDistanceVerifierTriangleTarget_proved
THEOREM PRCNullDistanceTransitiveTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean
PRCNullDistanceTransitiveTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean:214 
/-- The null-distance relation is transitive. -/
theorem PRCNullDistanceTransitiveTarget_proved :
    PRCNullDistanceTransitiveTarget :=
  PRCNullDistanceTransitiveTarget_of_triangle_modulus
    PRCJCostDistanceTriangleModulusTarget_proved
THEOREM prc_jcost_distance_increment_triangle_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean
prc_jcost_distance_increment_triangle_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean:246 
/-- The explicit rational increment estimate closes the whole J-cost
null-distance setoid chain. -/
theorem prc_jcost_distance_increment_triangle_certificate :
    PRCJCostDistanceIncrementTriangleCertificate where
  increment_formula := PRCJCostDistanceIncrementDisplay_formula
  increment_triangle := PRCJCostDistanceIncrementTriangleTarget_proved
  verifier_triangle := PRCJCostDistanceVerifierTriangleTarget_proved
  triangle_modulus := PRCJCostDistanceTriangleModulusTarget_proved
  null_distance_transitive := PRCNullDistanceTransitiveTarget_proved
  null_distance_setoid := PRCNullDistanceSetoidTarget_proved
  real_null_carrier := ⟨PRCRealNullClosed.ofRat 0⟩
  rat_embedding := ⟨PRCRealNullClosed.ofRat⟩

What this page does not claim

This module does not derive the cost function J from first principles; it assumes the cost structure and proves properties of its increment. This module does not construct the full ordered field of real numbers, only a carrier type with an embedding from rationals. This module does not claim that the increment formula is the only possible one; it proves the formula follows from the given definitions.

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