Foundation Primitive Recognition Calculus Recognizer Bridge

The recognizer bridge

The recognizer bridge (a formal bridge in the framework's machine-checked library of formal theorems) connects the primitive recognition calculus to the existing Law-of-Logic uniqueness theorem. It establishes that the cost assigned to a positive ratio in the primitive calculus is exactly the same as the cost function J(x) = (x + 1/x)/2 - 1 that the uniqueness theorem forces. This means the primitive calculus, which handles the discrete ledger of recognition events, is not a separate system; it is a surface that feeds into the same forced cost structure.

In plain terms, the bridge says: if you take any positive ratio r, the recognition cost assigned to it in the primitive calculus is (r + 1/r)/2 - 1. This is not a new assumption. It is a theorem that follows from the existing uniqueness result, which itself is proved from five plain conditions: reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. The bridge certificate, a formal structure in the library, records that this connection holds and names the remaining target: a fully native uniqueness proof for arbitrary costs in the primitive calculus itself.

The bridge is significant because it shows the primitive recognition calculus is not ad hoc. Its cost function is the same one that the framework's central theorem forces. This is a step toward unifying the primitive calculus with the broader Recognition Science structure, where the golden ratio phi emerges as the unique self-similar scaling and the eight-tick cycle follows. The bridge does not prove those later results, but it secures the foundation: the primitive calculus is anchored to the same forced cost.

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 bridge does not prove the golden ratio or the eight-tick cycle; it only secures the cost function connection. The bridge does not provide a native uniqueness proof for arbitrary costs in the primitive calculus; that remains a named target. The bridge does not introduce new axioms or assumptions; it relies on the existing uniqueness theorem.

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: