Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcjcost Distance Increment Triangle P

ARTICLE 4 claims 4 theorems

Foundation Primitive Recognition Calculus Prcjcost Distance Increment Triangle P

A single machine-checked proof shows that a specific cost formula satisfies the triangle inequality, a step toward building real numbers from recognition events.

Verify this page

The increment certificate

The triangle inequality is a basic property of distance: the direct path between two points is never longer than a path that goes through a third point. In the Recognition Science framework, distances are not given in advance but are built from a cost, a number that measures the price of recognizing one state from another. The declaration prc_jcost_distance_increment_triangle_certificate is a machine-checked proof that a particular cost increment obeys this inequality, and that this single fact is enough to complete a chain of constructions leading to a real-number system.

The certificate is a bundle of seven claims, each one proved in the framework's library of formal theorems. The first is an explicit formula: for a rational parameter t, the cost increment equals (t²)² / (2(1 + t²)). The remaining six are closure statements: the increment satisfies the triangle target, the verifier target, the triangle modulus target, the null-distance relation is transitive, the null-distance setoid is closed, and the resulting carrier is nonempty with an embedding from rationals. The final theorem assembles all seven into a single certificate, closing the chain that builds the PRC real carrier as Cauchy ledgers quotiented by null distance.

What the certificate does not claim is broader. It does not prove that the cost function J(x) = (x + 1/x)/2 - 1 is the unique cost satisfying the framework's axioms; that is a separate theorem. It does not claim that the triangle inequality holds for all possible costs, only for the specific increment formula stated. It does not assert that the real-number construction is complete or that it matches the classical real numbers; it only establishes the null-distance quotient carrier and its rational embedding. The certificate is a precise, narrow result: one formula, one inequality, and the structural consequences that follow from it.

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 PRCJCostDistanceIncrementTriangleTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean
PRCJCostDistanceIncrementTriangleTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean:93 
theorem PRCJCostDistanceIncrementTriangleTarget_proved :
    PRCJCostDistanceIncrementTriangleTarget := by
  intro eps heps
  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
  let four : PRCRat := two + two
  let rho : PRCRat := eps / (1 + eps)
  let eta : PRCRat := rho / four
  let delta : PRCRat := (eta * eta) / (four * (1 + eta))
  refine ⟨delta, ?_, ?_⟩
  · rw [PRCRat.positive_iff_toRat_pos]
    have heps_pos : (0 : ℚ) < eps.toRat := (PRCRat.positive_iff_toRat_pos eps).mp heps
    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.add two two).toRat = (4 : ℚ)
      rw [PRCRat.toRat_add]
      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 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 heta_pos : (0 : ℚ) < eta.toRat := by
      rw [PRCRat.toRat_div, hfour]
      have hrho_pos : (0 : ℚ) < rho.toRat := by
        rw [PRCRat.toRat_div, h_one_add_eps]
        positivity
      positivity
    rw [PRCRat.toRat_div, PRCRat.toRat_mul', PRCRat.toRat_mul',
      h_one_add_eta, hfour]
    positivity
  · intro p q hp hq
    have heps_pos : (0 : ℚ) < eps.toRat := (PRCRat.positive_iff_toRat_pos eps).mp heps
    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.add two two).toRat = (4 : ℚ)
      rw [PRCRat.toRat_add]
      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 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 hrho : rho.toRat = eps.toRat / (1 + eps.toRat) := by
      rw [PRCRat.toRat_div, h_one_add_eps]
    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 heta : eta.toRat = rho.toRat / 4 := by
      rw [PRCRat.toRat_div, hfour]
    have heta_pos : (0 : ℚ) < eta.toRat := by
      rw [heta]
      positivity
    have heta_lt_one : eta.toRat < 1 := by
      rw [heta]
      nlinarith
    have hdelta :
        delta.toRat = eta.toRat * eta.toRat / (4 * (1 + eta.toRat)) := by
      rw [PRCRat.toRat_div, PRCRat.toRat_mul', PRCRat.toRat_mul',
        h_one_add_eta, hfour]
    have hdelta_pos : (0 : ℚ) < delta.toRat := by
      rw [hdelta]
      positivity
    have hp_sq : p * p < eta.toRat := by
      exact sq_lt_of_display_lt_delta
        (t := p) (eta := eta.toRat) (delta := delta.toRat)
        heta_pos hdelta_pos (by rw [hdelta]) hp
    have hq_sq : q * q < eta.toRat := by
      exact sq_lt_of_display_lt_delta
        (t := q) (eta := eta.toRat) (delta := delta.toRat)
        heta_pos hdelta_pos (by rw [hdelta]) hq
    have hpq_sq_lt_rho : (p + q) * (p + q) < rho.toRat := by
      have hsq_bound : (p + q) * (p + q) ≤ 2 * (p * p) + 2 * (q * q) := by
        nlinarith [mul_self_nonneg (p - q)]
      rw [heta] at hp_sq hq_sq
      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]
    exact increment_display_lt_of_sq_lt
      (t := p + q) (eta := rho.toRat) (eps := eps.toRat)
      hrho_pos hrho_lt_one hpq_sq_lt_rho hrho_sq_half_lt_eps
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

The certificate does not prove the uniqueness of the cost function J(x) = (x + 1/x)/2 - 1. The certificate does not establish the triangle inequality for costs other than the specific increment formula. The certificate does not assert that the PRC real carrier is complete or isomorphic to the classical real numbers.

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