IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceTriangle

   1/-
   2  PrimitiveRecognitionCalculus/PRCJCostDistanceTriangle.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 9a: prove or isolate the local triangle modulus for
   9    `PRCJCostDistance`.
  10
  11  This pass translates the remaining PRC distance theorem into an exact
  12  verifier-rational inequality. No PRC object is redefined in verifier terms;
  13  the verifier formula is only a display theorem and blocker statement.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealNullSetoid
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- Verifier display of the J-cost square-gap distance. This is not the PRC
  24definition; it is the rational formula shown by `PRCJCostDistance_toRat`. -/
  25def PRCJCostDistanceRatDisplay (x y : ℚ) : ℚ :=
  26  let g : ℚ := 1 + (x - y) * (x - y)
  27  (g + g⁻¹) / 2 - 1
  28
  29/-- Display theorem for the PRC J-cost distance. -/
  30theorem PRCJCostDistance_toRat (a b : PRCRat) :
  31    (PRCJCostDistance a b).toRat =
  32      PRCJCostDistanceRatDisplay a.toRat b.toRat := by
  33  unfold PRCJCostDistance PRCJCostDistanceRatDisplay
  34  rw [PRCJCost.onPRCRat_toRat, PRCSquareGap_toRat]
  35
  36/-- Exact verifier-rational inequality still needed for the null-distance
  37quotient. It supplies a PRC rational `delta`, but the analytic estimate itself
  38is stated only on the conservative rational displays. -/
  39def PRCJCostDistanceVerifierTriangleTarget : Prop :=
  40  ∀ eps : PRCRat, PRCRat.positive eps →
  41    ∃ delta : PRCRat, PRCRat.positive delta ∧
  42      ∀ x y z : ℚ,
  43        PRCJCostDistanceRatDisplay x y < delta.toRat →
  44          PRCJCostDistanceRatDisplay y z < delta.toRat →
  45            PRCJCostDistanceRatDisplay x z < eps.toRat
  46
  47/-- The verifier-rational triangle inequality closes the PRC triangle-modulus
  48target by display transport. -/
  49theorem PRCJCostDistanceTriangleModulusTarget_of_verifier
  50    (h : PRCJCostDistanceVerifierTriangleTarget) :
  51    PRCJCostDistanceTriangleModulusTarget := by
  52  intro eps heps
  53  rcases h eps heps with ⟨delta, hdelta_pos, hdelta⟩
  54  refine ⟨delta, hdelta_pos, ?_⟩
  55  intro a b c hab hbc
  56  rw [PRCRat.lt_iff_toRat_lt] at hab hbc ⊢
  57  rw [PRCJCostDistance_toRat] at hab hbc ⊢
  58  exact hdelta a.toRat b.toRat c.toRat hab hbc
  59
  60/-- Once the verifier-rational inequality is proved, the final null-distance
  61setoid target follows. -/
  62theorem PRCNullDistanceSetoidTarget_of_verifier_triangle
  63    (h : PRCJCostDistanceVerifierTriangleTarget) :
  64    PRCNullDistanceSetoidTarget :=
  65  PRCNullDistanceSetoidTarget_of_triangle_modulus
  66    (PRCJCostDistanceTriangleModulusTarget_of_verifier h)
  67
  68/-- Conditional certificate for step 9a. The only remaining mathematical
  69problem is now the explicit rational inequality in
  70`PRCJCostDistanceVerifierTriangleTarget`. -/
  71structure PRCJCostDistanceTriangleConditionalCertificate : Prop where
  72  distance_display :
  73    ∀ a b : PRCRat,
  74      (PRCJCostDistance a b).toRat =
  75        PRCJCostDistanceRatDisplay a.toRat b.toRat
  76  verifier_triangle_target :
  77    PRCJCostDistanceVerifierTriangleTarget = PRCJCostDistanceVerifierTriangleTarget
  78  triangle_from_verifier :
  79    PRCJCostDistanceVerifierTriangleTarget → PRCJCostDistanceTriangleModulusTarget
  80  setoid_from_verifier :
  81    PRCJCostDistanceVerifierTriangleTarget → PRCNullDistanceSetoidTarget
  82
  83/-- Build Order step 9a conditional closure: PRC triangle transport is reduced
  84to the displayed rational inequality. -/
  85theorem prc_jcost_distance_triangle_conditional_certificate :
  86    PRCJCostDistanceTriangleConditionalCertificate where
  87  distance_display := PRCJCostDistance_toRat
  88  verifier_triangle_target := rfl
  89  triangle_from_verifier := PRCJCostDistanceTriangleModulusTarget_of_verifier
  90  setoid_from_verifier := PRCNullDistanceSetoidTarget_of_verifier_triangle
  91
  92end PrimitiveRecognitionCalculus
  93end Foundation
  94end IndisputableMonolith
  95