Foundation Primitive Recognition Calculus Recognizer Bridge Cost To Rat

The cost in plain numbers

In the Recognition Science framework, a ledger, a discrete record of events, tracks comparisons between quantities. The basic comparison is a ratio: two positive numbers written as one divided by the other. The framework assigns each positive ratio a recognition cost, a number that says how expensive it is for the ledger to tell the two quantities apart. The declaration cost_toRat is the precise statement of that cost in ordinary rational arithmetic.

The theorem says that for any positive ratio r, the cost equals (r + 1/r)/2 - 1. In words: add the ratio to its reciprocal, divide by two, subtract one. The reciprocal term 1/r is the ratio reversed, so the cost treats a ratio and its inverse symmetrically. A ratio of 1, where the two quantities are equal, costs zero: no recognition is needed. A ratio of 2 costs (2 + 1/2)/2 - 1 = 0.25. A ratio of 3 costs (3 + 1/3)/2 - 1 ≈ 0.667. The cost grows as the ratio moves away from 1 in either direction.

This formula is not a definitional choice. It is a proved theorem in the framework's machine-checked library of formal theorems, derived from the cost function, the ledger's measure of comparison expense, defined on positive ratios. A companion theorem shows the same rational cost agrees with the real-valued cost function J(x) = (x + 1/x)/2 - 1 that appears in the framework's central uniqueness result. The bridge statement packages this agreement: any continuous cost function satisfying the framework's five conditions must equal J. The cost_toRat declaration is the rational-arithmetic face of that same J.

What the declaration does not claim is just as important. It does not say that recognition costs in general must take this form; that stronger uniqueness claim, for arbitrary cost functions without the continuity condition, remains an open target in the framework. It does not assign physical meaning to any particular ratio or cost value. It does not say that the framework's ledger is the only way to model comparison, only that within this framework, the cost of a positive ratio is exactly this number.

theorem cost_toRat (r : PRCPositiveRatio) :
    r.cost.toRat = (r.value.toRat + r.value.toRat⁻¹) / 2 - 1 :=
  PRCJCost.onPRCRat_toRat r.value

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

That all recognition costs must take this form without further conditions. That any particular ratio or cost value has physical meaning. That the framework's ledger is the only way to model comparison.

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: