IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealNullSetoid

   1/-
   2  PrimitiveRecognitionCalculus/RealNullSetoid.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 9: promote the first Cauchy-ledger carrier toward the
   9    final null-distance quotient.
  10
  11  This pass isolates the exact analytic blocker. The quotient bookkeeping is
  12  closed conditionally: a local triangle modulus for `PRCJCostDistance` implies
  13  `PRCNullEquivalent` is transitive, hence a setoid.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCauchy
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- Exact analytic blocker for the null-distance quotient. It says the
  24J-cost-derived rational distance has a local triangle modulus: for each
  25positive tolerance there is a positive smaller tolerance so that two small
  26legs force the composed leg below the original tolerance. -/
  27def PRCJCostDistanceTriangleModulusTarget : Prop :=
  28  ∀ eps : PRCRat, PRCRat.positive eps →
  29    ∃ delta : PRCRat, PRCRat.positive delta ∧
  30      ∀ a b c : PRCRat,
  31        PRCRat.lt (PRCJCostDistance a b) delta →
  32          PRCRat.lt (PRCJCostDistance b c) delta →
  33            PRCRat.lt (PRCJCostDistance a c) eps
  34
  35/-- The analytic triangle modulus is sufficient for null-distance
  36transitivity. All remaining work here is completed-orbit index bookkeeping. -/
  37theorem PRCNullDistanceTransitiveTarget_of_triangle_modulus
  38    (htri : PRCJCostDistanceTriangleModulusTarget) :
  39    PRCNullDistanceTransitiveTarget := by
  40  intro u v w huv hvw eps heps
  41  rcases htri eps heps with ⟨delta, hdelta_pos, hdelta⟩
  42  rcases huv delta hdelta_pos with ⟨Nuv, hNuv⟩
  43  rcases hvw delta hdelta_pos with ⟨Nvw, hNvw⟩
  44  refine ⟨max Nuv Nvw, ?_⟩
  45  intro n hn
  46  have hn_uv : Nuv ≤ n := le_trans (Nat.le_max_left Nuv Nvw) hn
  47  have hn_vw : Nvw ≤ n := le_trans (Nat.le_max_right Nuv Nvw) hn
  48  exact hdelta (u.term n) (v.term n) (w.term n)
  49    (hNuv n hn_uv) (hNvw n hn_vw)
  50
  51/-- A transitivity proof turns `PRCNullEquivalent` into a setoid. -/
  52def PRCNullDistanceSetoidOfTransitive
  53    (htrans : PRCNullDistanceTransitiveTarget) : Setoid PRCCauchySeq where
  54  r := PRCNullEquivalent
  55  iseqv := by
  56    constructor
  57    · exact PRCNullEquivalent.refl
  58    · intro u v
  59      exact PRCNullEquivalent.symm
  60    · intro u v w
  61      exact htrans u v w
  62
  63/-- Conditional final real carrier: once the analytic triangle modulus is
  64proved, this is the intended PRC real quotient by null distance. -/
  65def PRCRealNull (htrans : PRCNullDistanceTransitiveTarget) : Type :=
  66  Quot (PRCNullDistanceSetoidOfTransitive htrans)
  67
  68namespace PRCRealNull
  69
  70/-- Embed a rational as a null-distance quotient class, conditional on the
  71transitivity proof. -/
  72def ofRat (htrans : PRCNullDistanceTransitiveTarget) (q : PRCRat) :
  73    PRCRealNull htrans :=
  74  Quot.mk (PRCNullDistanceSetoidOfTransitive htrans) (PRCCauchySeq.constant q)
  75
  76end PRCRealNull
  77
  78/-- The exact setoid target follows from transitivity. -/
  79theorem PRCNullDistanceSetoidTarget_of_transitive
  80    (htrans : PRCNullDistanceTransitiveTarget) :
  81    PRCNullDistanceSetoidTarget := by
  82  exact (PRCNullDistanceSetoidOfTransitive htrans).iseqv
  83
  84/-- The exact setoid target follows from the sharper triangle-modulus target. -/
  85theorem PRCNullDistanceSetoidTarget_of_triangle_modulus
  86    (htri : PRCJCostDistanceTriangleModulusTarget) :
  87    PRCNullDistanceSetoidTarget :=
  88  PRCNullDistanceSetoidTarget_of_transitive
  89    (PRCNullDistanceTransitiveTarget_of_triangle_modulus htri)
  90
  91/-- K1/R9. Audit record: the final null-distance quotient still lives under
  92trace closure; the open obligation is analytic, not a new primitive. -/
  93def realNullSetoidClaim : StrengthClaim where
  94  label := "BuildOrder9_real_null_distance_setoid"
  95  tag := StrengthTag.traceClosure
  96  statement :=
  97    "The PRC real null-distance setoid follows from the J-cost distance triangle modulus."
  98
  99/-- Conditional certificate for Build Order step 9. It records the precise
 100remaining theorem and proves that this theorem is sufficient to construct the
 101null-distance setoid and quotient carrier. -/
 102structure PRCRealNullSetoidConditionalCertificate : Prop where
 103  triangle_modulus_target :
 104    PRCJCostDistanceTriangleModulusTarget = PRCJCostDistanceTriangleModulusTarget
 105  transitive_from_triangle :
 106    PRCJCostDistanceTriangleModulusTarget → PRCNullDistanceTransitiveTarget
 107  setoid_from_transitive :
 108    PRCNullDistanceTransitiveTarget → PRCNullDistanceSetoidTarget
 109  setoid_from_triangle :
 110    PRCJCostDistanceTriangleModulusTarget → PRCNullDistanceSetoidTarget
 111  quotient_from_transitive :
 112    ∀ htrans : PRCNullDistanceTransitiveTarget, Nonempty (PRCRealNull htrans)
 113  rat_embedding_from_transitive :
 114    ∀ htrans : PRCNullDistanceTransitiveTarget, Nonempty (PRCRat → PRCRealNull htrans)
 115  strength_tag : realNullSetoidClaim.tag = StrengthTag.traceClosure
 116
 117/-- Build Order step 9 conditional closure: no quotient mechanics remain once
 118the local J-cost triangle modulus is proved. -/
 119theorem real_null_setoid_conditional_certificate :
 120    PRCRealNullSetoidConditionalCertificate where
 121  triangle_modulus_target := rfl
 122  transitive_from_triangle := PRCNullDistanceTransitiveTarget_of_triangle_modulus
 123  setoid_from_transitive := PRCNullDistanceSetoidTarget_of_transitive
 124  setoid_from_triangle := PRCNullDistanceSetoidTarget_of_triangle_modulus
 125  quotient_from_transitive := by
 126    intro htrans
 127    exact ⟨PRCRealNull.ofRat htrans 0⟩
 128  rat_embedding_from_transitive := by
 129    intro htrans
 130    exact ⟨PRCRealNull.ofRat htrans⟩
 131  strength_tag := rfl
 132
 133end PrimitiveRecognitionCalculus
 134end Foundation
 135end IndisputableMonolith
 136