Foundation Primitive Recognition Calculus Prcjcost Distance Verifier Triangle

The verifier triangle

The triangle inequality is the rule that the direct path between two points is never longer than a path that stops somewhere else. In ordinary geometry, the distance from A to B is always at most the distance from A to C plus the distance from C to B. A distance that obeys this rule behaves like a ruler; one that does not can still be useful, but it cannot support the usual ideas of straightness, circles, or shortest paths.

Recognition Science builds its geometry from a ledger, a discrete record of recognition events, and a forced cost for each event. The cost function J(x) = (x + 1/x)/2 - 1 is proved to be the only one satisfying five plain conditions, and from it the framework defines a distance between two rational numbers. The distance between x and y is J(x - y), so it depends only on the difference between the endpoints, not on where they sit. This translation invariance is already proved in the framework's machine-checked library of formal theorems.

The open question is whether this distance obeys the triangle inequality. The framework has reduced that question to a sharper one: if two small increments each have small J-cost, does their sum also have small J-cost? This increment-only version is the mathematical core of the verifier triangle target. The framework has proved that this increment-only target implies the full three-endpoint triangle inequality, and that the triangle inequality in turn closes the whole null-distance equivalence chain, the step that would let the framework treat points at zero distance as the same point.

What remains is a single one-dimensional estimate about how J-costs add. The framework has packaged this as a conditional certificate: a structure that holds all the proved implications, waiting only for the increment-only modulus target. In plain language, the framework has shown that the entire geometric structure depends on one last inequality about how small costs combine. Proving that inequality is the remaining target; the framework has already proved everything that would follow from it.

/-- The displayed distance is translation-invariant: it depends only on the
increment between the endpoints. -/
theorem PRCJCostDistanceRatDisplay_as_increment (x y : ℚ) :
    PRCJCostDistanceRatDisplay x y =
      PRCJCostDistanceIncrementDisplay (x - y) := by
  simp [PRCJCostDistanceIncrementDisplay, PRCJCostDistanceRatDisplay]
  ring_nf

/-- The increment-only triangle target implies the verifier-rational
three-endpoint triangle target. -/
theorem PRCJCostDistanceVerifierTriangleTarget_of_increment
    (h : PRCJCostDistanceIncrementTriangleTarget) :
    PRCJCostDistanceVerifierTriangleTarget := by
  intro eps heps
  rcases h eps heps with ⟨delta, hdelta_pos, hdelta⟩
  refine ⟨delta, hdelta_pos, ?_⟩
  intro x y z hxy hyz
  have hxy' :
      PRCJCostDistanceIncrementDisplay (x - y) < delta.toRat := by
    rwa [PRCJCostDistanceRatDisplay_as_increment] at hxy
  have hyz' :
      PRCJCostDistanceIncrementDisplay (y - z) < delta.toRat := by
    rwa [PRCJCostDistanceRatDisplay_as_increment] at hyz
  have hsum :
      PRCJCostDistanceIncrementDisplay ((x - y) + (y - z)) < eps.toRat :=
    hdelta (x - y) (y - z) hxy' hyz'
  have hxz :
      PRCJCostDistanceRatDisplay x z =
        PRCJCostDistanceIncrementDisplay ((x - y) + (y - z)) := by
    rw [PRCJCostDistanceRatDisplay_as_increment]
    congr
    ring
  rwa [hxz]

/-- The increment-only blocker closes the whole PRC null-distance setoid chain. -/
theorem PRCNullDistanceSetoidTarget_of_increment_triangle
    (h : PRCJCostDistanceIncrementTriangleTarget) :
    PRCNullDistanceSetoidTarget :=
  PRCNullDistanceSetoidTarget_of_verifier_triangle
    (PRCJCostDistanceVerifierTriangleTarget_of_increment h)

What this page does not claim

The increment-only modulus target is not proved; it is stated as an open target. The framework does not claim that the J-cost distance is a metric in the classical sense, only that the triangle inequality would close the equivalence chain. This module does not define the full geometry of Recognition Science; it establishes the conditional implications for one distance property.

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