Foundation Primitive Recognition Calculus Recognizer Bridge Cost To Real Jcost

The bridge to real costs

A recognition event, in this framework, is a discrete record of a comparison between two things. The ledger keeps these records as exact ratios. The declaration cost_toReal_jcost is a bridge: it shows that the cost assigned to one of these ratios, when converted from the ledger's exact number system to ordinary real numbers, is exactly the same as the value of a known real-valued function called Jcost.

The formula is J(x) = (x + 1/x)/2 - 1. For a ratio r, the theorem states that the ledger's cost, written as a real number, equals J(r). The proof is a direct calculation: it expands the definition of the ledger cost, substitutes the formula for Jcost, and simplifies. The machine-checked library of formal theorems verifies each step.

This bridge matters because the real-valued Jcost function is the subject of a separate uniqueness theorem. That theorem says that any real function satisfying five plain conditions (reciprocal symmetry, zero cost at unity, a forced composition law, calibration, continuity) must equal Jcost. The bridge connects the discrete ledger to that theorem, but it does not prove that the ledger itself satisfies those five conditions.

In Recognition Science, the framework models the ledger's cost as a discrete exact ratio, while the uniqueness theorem works with continuous real functions. The bridge shows the two agree wherever the discrete cost is defined. It is a step toward a fully native uniqueness proof for the discrete case, but that native proof remains a named target, not a finished result.

What the declaration does not claim is just as important. It does not claim that the ledger's cost function is the only possible one; that would require the discrete uniqueness proof. It does not claim that the five conditions hold for the ledger; it only shows the values match where the discrete cost is defined. And it does not claim anything about the physical world, such as particle masses or the fine-structure constant. Those are separate empirical checks, not consequences of this bridge.

theorem cost_toReal_jcost (r : PRCPositiveRatio) :
    (r.cost.toRat : ℝ) = Cost.Jcost ((r.value.toRat : ℚ) : ℝ) := by
  rw [cost_toRat]
  unfold Cost.Jcost
  rw [Rat.cast_sub, Rat.cast_div, Rat.cast_add, Rat.cast_inv]
  norm_num

theorem PRCRecognizerLawOfLogicBridgeTarget_proved :
    PRCRecognizerLawOfLogicBridgeTarget := by
  intro F hA hR hN hC hCal hCont x hx
  exact PRCJCost.bridge_to_existing_jcost_uniqueness
    F hA hR hN hC hCal hCont x hx

What this page does not claim

The discrete ledger cost is the only possible cost function. The five conditions of the real uniqueness theorem hold for the discrete ledger. The bridge implies any physical constant such as the fine-structure constant.

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