Foundation Primitive Recognition Calculus Real Cauchy Prcjcost Distance Symmetri

A symmetric measure of difference

A distance function answers a simple question: how far apart are two things? The usual answer for numbers, absolute difference, treats its two inputs the same way. The distance from 3 to 7 is 4, and the distance from 7 to 3 is also 4. This property, symmetry, is so ordinary that it is easy to miss that not every measure of difference has it. The declaration PRCJCostDistance_symmetric is a machine-checked proof that a specific, more elaborate measure of difference also has this property.

That measure, called PRCJCostDistance, is built inside the Recognition Science framework. It takes two rational numbers and computes a cost: one plus the square of their difference. The cost is not simply the gap; it is a transformed version that grows faster than the gap itself. The theorem proves that this cost is symmetric: the cost of moving from a to b equals the cost of moving from b to a. The proof is short and direct, using the fact that squaring a number and squaring its negative give the same result.

This symmetry is not a curiosity. The same cost function appears in the framework's definition of a Cauchy sequence, a sequence whose terms get arbitrarily close to each other. The symmetry property is what makes the framework's notion of "getting close" well-behaved: if one term is close to another, the relationship does not depend on which term you look at first. The framework uses this to build its version of real numbers, the continuous number line, from rational building blocks.

The theorem is a formal statement, checked by a machine, that this symmetry holds for all rational inputs. It does not claim that the cost function is a distance in the usual metric sense; it does not prove the triangle inequality, and it does not show that the cost is zero only when the inputs are equal. Those are separate properties, and the framework does not assert them here.

theorem PRCJCostDistance_symmetric (a b : PRCRat) :
    PRCJCostDistance a b = PRCJCostDistance b a := by
  apply PRCRat.toRat_injective
  unfold PRCJCostDistance
  rw [PRCJCost.onPRCRat_toRat, PRCJCost.onPRCRat_toRat,
    PRCSquareGap_toRat, PRCSquareGap_toRat]
  ring

/-- J-cost distance used by the first PRC Cauchy surface. It sends additive
separation through the positive ratio `1 + (a-b)^2`, then applies the PRC
rational J-cost. -/
def PRCJCostDistance (a b : PRCRat) : PRCRat :=
  PRCJCost.onPRCRat (PRCSquareGap a b)

What this page does not claim

The theorem does not prove the triangle inequality for the cost function. The theorem does not show that the cost is zero only when the two inputs are equal. The theorem does not claim the cost function is a metric in the standard sense.

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