IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RecognizerBridge

   1/-
   2  PrimitiveRecognitionCalculus/RecognizerBridge.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 14: produce the positive-ratio recognizer surface from
   9    PRC cost theory and map it into the existing Law-of-Logic J-cost chain.
  10
  11  The positive-ratio recognizer is PRC-native. The existing continuous
  12  uniqueness theorem is still recorded as a classical-extension bridge because
  13  it quantifies over positive real ratios and continuity.
  14-/
  15
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Inevitability
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- Positive PRC ratios are the input surface for recognizer comparisons. -/
  24structure PRCPositiveRatio where
  25  value : PRCRat
  26  positive : PRCRat.positive value
  27
  28namespace PRCPositiveRatio
  29
  30/-- The canonical positive unit ratio. -/
  31def one : PRCPositiveRatio where
  32  value := 1
  33  positive := by
  34    rw [PRCRat.positive_iff_toRat_pos]
  35    change 0 < PRCRat.one.toRat
  36    rw [PRCRat.one_toRat]
  37    norm_num
  38
  39/-- The quotient-level PRC J-cost assigned to a positive ratio. -/
  40def cost (r : PRCPositiveRatio) : PRCRat :=
  41  PRCJCost.onPRCRat r.value
  42
  43theorem cost_toRat (r : PRCPositiveRatio) :
  44    r.cost.toRat = (r.value.toRat + r.value.toRat⁻¹) / 2 - 1 :=
  45  PRCJCost.onPRCRat_toRat r.value
  46
  47theorem cost_toReal_jcost (r : PRCPositiveRatio) :
  48    (r.cost.toRat : ℝ) = Cost.Jcost ((r.value.toRat : ℚ) : ℝ) := by
  49  rw [cost_toRat]
  50  unfold Cost.Jcost
  51  rw [Rat.cast_sub, Rat.cast_div, Rat.cast_add, Rat.cast_inv]
  52  norm_num
  53
  54end PRCPositiveRatio
  55
  56/-- Recognition cost on a positive PRC ratio. -/
  57def PRCRecognitionCost (r : PRCPositiveRatio) : PRCRat :=
  58  r.cost
  59
  60theorem PRCRecognitionCost_display (r : PRCPositiveRatio) :
  61    (PRCRecognitionCost r).toRat =
  62      (r.value.toRat + r.value.toRat⁻¹) / 2 - 1 :=
  63  PRCPositiveRatio.cost_toRat r
  64
  65/-- Exact bridge target from PRC recognizer costs into the existing
  66Law-of-Logic uniqueness theorem. -/
  67def PRCRecognizerLawOfLogicBridgeTarget : Prop :=
  68  ∀ (F : ℝ → ℝ),
  69    Cost.FunctionalEquation.AczelSmoothnessPackage →
  70    Cost.FunctionalEquation.IsReciprocalCost F →
  71    Cost.FunctionalEquation.IsNormalized F →
  72    Cost.FunctionalEquation.SatisfiesCompositionLaw F →
  73    Cost.FunctionalEquation.IsCalibrated F →
  74    ContinuousOn F (Set.Ioi 0) →
  75    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x
  76
  77theorem PRCRecognizerLawOfLogicBridgeTarget_proved :
  78    PRCRecognizerLawOfLogicBridgeTarget := by
  79  intro F hA hR hN hC hCal hCont x hx
  80  exact PRCJCost.bridge_to_existing_jcost_uniqueness
  81    F hA hR hN hC hCal hCont x hx
  82
  83/-- Step 14 certificate. The recognizer surface is closed through the existing
  84continuous Law-of-Logic bridge; fully native arbitrary-cost uniqueness remains
  85the named PRC target from `PRCJCost.lean`. -/
  86structure PRCRecognizerBridgeCertificate : Prop where
  87  positive_ratio_surface : Nonempty PRCPositiveRatio
  88  recognition_cost_surface : Nonempty (PRCPositiveRatio → PRCRat)
  89  cost_display :
  90    ∀ r : PRCPositiveRatio,
  91      (PRCRecognitionCost r).toRat =
  92        (r.value.toRat + r.value.toRat⁻¹) / 2 - 1
  93  real_jcost_bridge :
  94    ∀ r : PRCPositiveRatio,
  95      ((PRCRecognitionCost r).toRat : ℝ) =
  96        Cost.Jcost ((r.value.toRat : ℚ) : ℝ)
  97  law_of_logic_bridge : PRCRecognizerLawOfLogicBridgeTarget
  98  native_uniqueness_target_named :
  99    PRCJCost.PRCNativeCostUniquenessTarget =
 100      PRCJCost.PRCNativeCostUniquenessTarget
 101  strength_tag : StrengthTag.classicalExtension = StrengthTag.classicalExtension
 102
 103theorem prc_recognizer_bridge_certificate :
 104    PRCRecognizerBridgeCertificate where
 105  positive_ratio_surface := ⟨PRCPositiveRatio.one⟩
 106  recognition_cost_surface := ⟨PRCRecognitionCost⟩
 107  cost_display := PRCRecognitionCost_display
 108  real_jcost_bridge := by
 109    intro r
 110    exact PRCPositiveRatio.cost_toReal_jcost r
 111  law_of_logic_bridge := PRCRecognizerLawOfLogicBridgeTarget_proved
 112  native_uniqueness_target_named := rfl
 113  strength_tag := rfl
 114
 115end PrimitiveRecognitionCalculus
 116end Foundation
 117end IndisputableMonolith
 118