IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceVerifierTriangle

   1/-
   2  PrimitiveRecognitionCalculus/PRCJCostDistanceVerifierTriangle.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 9b: prove or isolate the verifier-rational triangle
   9    inequality for the displayed J-cost distance.
  10
  11  This pass removes endpoint bookkeeping. The displayed distance depends only
  12  on the rational increment, so the remaining blocker is an additive two-leg
  13  modulus for increments `p` and `q`.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceTriangle
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- One-increment display of the rational J-cost distance. -/
  24def PRCJCostDistanceIncrementDisplay (t : ℚ) : ℚ :=
  25  PRCJCostDistanceRatDisplay 0 t
  26
  27/-- The displayed distance is translation-invariant: it depends only on the
  28increment between the endpoints. -/
  29theorem PRCJCostDistanceRatDisplay_as_increment (x y : ℚ) :
  30    PRCJCostDistanceRatDisplay x y =
  31      PRCJCostDistanceIncrementDisplay (x - y) := by
  32  simp [PRCJCostDistanceIncrementDisplay, PRCJCostDistanceRatDisplay]
  33  ring_nf
  34
  35/-- Sharper exact blocker: an additive two-leg modulus for rational increments.
  36This is the mathematical core behind the three-endpoint verifier triangle
  37target. -/
  38def PRCJCostDistanceIncrementTriangleTarget : Prop :=
  39  ∀ eps : PRCRat, PRCRat.positive eps →
  40    ∃ delta : PRCRat, PRCRat.positive delta ∧
  41      ∀ p q : ℚ,
  42        PRCJCostDistanceIncrementDisplay p < delta.toRat →
  43          PRCJCostDistanceIncrementDisplay q < delta.toRat →
  44            PRCJCostDistanceIncrementDisplay (p + q) < eps.toRat
  45
  46/-- The increment-only triangle target implies the verifier-rational
  47three-endpoint triangle target. -/
  48theorem PRCJCostDistanceVerifierTriangleTarget_of_increment
  49    (h : PRCJCostDistanceIncrementTriangleTarget) :
  50    PRCJCostDistanceVerifierTriangleTarget := by
  51  intro eps heps
  52  rcases h eps heps with ⟨delta, hdelta_pos, hdelta⟩
  53  refine ⟨delta, hdelta_pos, ?_⟩
  54  intro x y z hxy hyz
  55  have hxy' :
  56      PRCJCostDistanceIncrementDisplay (x - y) < delta.toRat := by
  57    rwa [PRCJCostDistanceRatDisplay_as_increment] at hxy
  58  have hyz' :
  59      PRCJCostDistanceIncrementDisplay (y - z) < delta.toRat := by
  60    rwa [PRCJCostDistanceRatDisplay_as_increment] at hyz
  61  have hsum :
  62      PRCJCostDistanceIncrementDisplay ((x - y) + (y - z)) < eps.toRat :=
  63    hdelta (x - y) (y - z) hxy' hyz'
  64  have hxz :
  65      PRCJCostDistanceRatDisplay x z =
  66        PRCJCostDistanceIncrementDisplay ((x - y) + (y - z)) := by
  67    rw [PRCJCostDistanceRatDisplay_as_increment]
  68    congr
  69    ring
  70  rwa [hxz]
  71
  72/-- The increment-only blocker closes the whole PRC null-distance setoid chain. -/
  73theorem PRCNullDistanceSetoidTarget_of_increment_triangle
  74    (h : PRCJCostDistanceIncrementTriangleTarget) :
  75    PRCNullDistanceSetoidTarget :=
  76  PRCNullDistanceSetoidTarget_of_verifier_triangle
  77    (PRCJCostDistanceVerifierTriangleTarget_of_increment h)
  78
  79/-- Conditional certificate for step 9b. The only remaining theorem is now the
  80increment-only modulus target. -/
  81structure PRCJCostDistanceVerifierTriangleConditionalCertificate : Prop where
  82  translation_invariance :
  83    ∀ x y : ℚ,
  84      PRCJCostDistanceRatDisplay x y =
  85        PRCJCostDistanceIncrementDisplay (x - y)
  86  increment_triangle_target :
  87    PRCJCostDistanceIncrementTriangleTarget = PRCJCostDistanceIncrementTriangleTarget
  88  verifier_from_increment :
  89    PRCJCostDistanceIncrementTriangleTarget → PRCJCostDistanceVerifierTriangleTarget
  90  setoid_from_increment :
  91    PRCJCostDistanceIncrementTriangleTarget → PRCNullDistanceSetoidTarget
  92
  93/-- Build Order step 9b conditional closure: the verifier triangle target is
  94reduced to a one-dimensional additive increment estimate. -/
  95theorem prc_jcost_distance_verifier_triangle_conditional_certificate :
  96    PRCJCostDistanceVerifierTriangleConditionalCertificate where
  97  translation_invariance := PRCJCostDistanceRatDisplay_as_increment
  98  increment_triangle_target := rfl
  99  verifier_from_increment := PRCJCostDistanceVerifierTriangleTarget_of_increment
 100  setoid_from_increment := PRCNullDistanceSetoidTarget_of_increment_triangle
 101
 102end PrimitiveRecognitionCalculus
 103end Foundation
 104end IndisputableMonolith
 105