Foundation Primitive Recognition Calculus Recognizer Bridge Prcpositive Ratio

The positive ratio surface

A positive ratio is a comparison of two quantities where the first is greater than zero, written as a fraction. The framework's declaration PRCPositiveRatio packages this idea as a formal object: it pairs a ratio value with a proof that the value is positive. This matters because recognition costs, the framework's central accounting device, are only defined on positive inputs. The declaration also provides the canonical unit ratio, the value 1, as the distinguished starting point for all comparisons.

The framework then attaches a cost to any positive ratio. The cost is not chosen freely; it is forced by the framework's proved uniqueness theorem. The declaration PRCPositiveRatio.cost defines this cost, and the theorem cost_toRat shows the explicit formula: for a ratio r, the cost equals (r + 1/r)/2 - 1. This is the same J-cost function that the framework's Law-of-Logic theorem derives from five plain conditions: reciprocal symmetry, zero cost at unity, a composition law, calibration, and continuity. The bridge theorem PRCRecognizerLawOfLogicBridgeTarget_proved confirms that any function satisfying those conditions must equal this J-cost on all positive inputs.

The declaration also records what the framework calls a bridge certificate. This certificate states that the recognizer surface, the collection of positive ratios and their costs, is closed through the existing continuous Law-of-Logic bridge. In plain terms: the framework has a machine-checked proof that its recognition cost formula matches the uniqueness theorem for all positive ratios. The certificate names a target for future work: a fully native uniqueness proof that does not rely on the continuous bridge, which remains open.

What the declaration does not claim is equally precise. It does not claim that the cost formula is the only possible cost; it claims that the formula is forced once the five conditions hold. It does not claim that the bridge certificate proves native uniqueness; the certificate explicitly names that as a target. It does not claim any physical measurement or empirical content; the declaration is purely formal, establishing a mathematical fact about costs on positive ratios.

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

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

theorem prc_recognizer_bridge_certificate :
    PRCRecognizerBridgeCertificate where
  positive_ratio_surface := ⟨PRCPositiveRatio.one⟩
  recognition_cost_surface := ⟨PRCRecognitionCost⟩
  cost_display := PRCRecognitionCost_display
  real_jcost_bridge := by
    intro r
    exact PRCPositiveRatio.cost_toReal_jcost r
  law_of_logic_bridge := PRCRecognizerLawOfLogicBridgeTarget_proved
  native_uniqueness_target_named := rfl
  strength_tag := rfl

What this page does not claim

The declaration does not prove native uniqueness without the continuous bridge; it names that as a target. The declaration does not claim the cost formula is the only possible cost without the five conditions. The declaration does not contain any empirical or measured content.

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: