IndisputableMonolith.Verification.CPT.ForcedFactorization

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Verification.CPT.Core
   4
   5/-!
   6# CPT Forced Factorization (Hypothesis-Explicit Lean Layer)
   7
   8This module captures the strongest currently defensible Lean shape for the paper's
   9forced-factorization claims:
  10
  11- ratio-induced canonical cost scaffold,
  12- certificate hypotheses stated explicitly,
  13- existence of a reparametrization on the realized cost image,
  14- state-independence only under an explicit rigidity hypothesis.
  15
  16No hidden assumptions are used.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Verification
  21namespace CPT
  22namespace ForcedFactorization
  23
  24open scoped Classical
  25
  26variable {S O : Type}
  27
  28/-- Ratio-cost scaffold used by CPT factorization statements. -/
  29structure RatioCostSpace (S O : Type) where
  30  iotaS : S → ℝ
  31  iotaO : O → ℝ
  32  iotaS_pos : ∀ s : S, 0 < iotaS s
  33  iotaO_pos : ∀ o : O, 0 < iotaO o
  34
  35namespace RatioCostSpace
  36
  37/-- Ratio coordinate entering the canonical reciprocal cost. -/
  38noncomputable def ratio (R : RatioCostSpace S O) (s : S) (o : O) : ℝ :=
  39  R.iotaS s / R.iotaO o
  40
  41/-- Canonical ratio-induced cost used in CPT factorization arguments. -/
  42noncomputable def canonicalCost (R : RatioCostSpace S O) (s : S) (o : O) : ℝ :=
  43  IndisputableMonolith.Cost.Jcost (ratio R s o)
  44
  45/-- Realized image of the canonical cost on `S × O`. -/
  46def CostImage (R : RatioCostSpace S O) : Set ℝ :=
  47  Set.range (fun p : S × O => canonicalCost R p.1 p.2)
  48
  49/-- Encoded realized-cost coordinate used for reparametrization witnesses. -/
  50abbrev CostCode (R : RatioCostSpace S O) := {t : ℝ // t ∈ CostImage R}
  51
  52end RatioCostSpace
  53
  54open RatioCostSpace
  55
  56/-- Explicit assumptions used for the factorization and monotone reparametrization layer. -/
  57structure CertificateHypotheses
  58    (R : RatioCostSpace S O) (C : S → O → ℝ) : Prop where
  59  /-- Ratio-level dependence: equal ratio coordinate implies equal certificate value. -/
  60  depends_on_ratio :
  61    ∀ {s1 s2 : S} {o1 o2 : O},
  62      ratio R s1 o1 = ratio R s2 o2 → C s1 o1 = C s2 o2
  63  /-- Cost-level dependence (stronger; used for image reparametrization existence). -/
  64  depends_on_cost :
  65    ∀ {s1 s2 : S} {o1 o2 : O},
  66      canonicalCost R s1 o1 = canonicalCost R s2 o2 → C s1 o1 = C s2 o2
  67  /-- Monotonicity in the canonical cost ordering for fixed `s`. -/
  68  monotone_in_cost :
  69    ∀ (s : S) (o1 o2 : O),
  70      canonicalCost R s o1 ≤ canonicalCost R s o2 → C s o1 ≤ C s o2
  71
  72/-- Explicit rigidity bundle used to force independence from the state variable. -/
  73structure RigidityHypotheses
  74    (R : RatioCostSpace S O) (C : S → O → ℝ) : Prop where
  75  independent_of_state : ∀ (s1 s2 : S) (o : O), C s1 o = C s2 o
  76
  77/-- More primitive hypothesis bundle for the cost-reparametrization layer.
  78`depends_on_cost` is derived from ratio-level dependence plus a cost-to-ratio bridge. -/
  79structure PrimitiveCertificateHypotheses
  80    (R : RatioCostSpace S O) (C : S → O → ℝ) : Prop where
  81  depends_on_ratio :
  82    ∀ {s1 s2 : S} {o1 o2 : O},
  83      ratio R s1 o1 = ratio R s2 o2 → C s1 o1 = C s2 o2
  84  ratio_of_cost_eq :
  85    ∀ {s1 s2 : S} {o1 o2 : O},
  86      canonicalCost R s1 o1 = canonicalCost R s2 o2 →
  87        ratio R s1 o1 = ratio R s2 o2
  88  monotone_in_cost :
  89    ∀ (s : S) (o1 o2 : O),
  90      canonicalCost R s o1 ≤ canonicalCost R s o2 → C s o1 ≤ C s o2
  91
  92/-- Primitive rigidity hypothesis phrased at ratio level:
  93for fixed `o`, ratios collapse across states. -/
  94structure PrimitiveRigidityHypotheses
  95    (R : RatioCostSpace S O) : Prop where
  96  ratio_state_collapse : ∀ (s1 s2 : S) (o : O), ratio R s1 o = ratio R s2 o
  97
  98theorem primitive_to_certificate
  99    (R : RatioCostSpace S O) (C : S → O → ℝ)
 100    (hPrim : PrimitiveCertificateHypotheses R C) :
 101    CertificateHypotheses R C := by
 102  refine
 103    { depends_on_ratio := hPrim.depends_on_ratio
 104      depends_on_cost := ?_
 105      monotone_in_cost := hPrim.monotone_in_cost }
 106  intro s1 s2 o1 o2 hCost
 107  exact hPrim.depends_on_ratio (hPrim.ratio_of_cost_eq hCost)
 108
 109theorem primitive_to_rigidity
 110    (R : RatioCostSpace S O) (C : S → O → ℝ)
 111    (hPrim : PrimitiveCertificateHypotheses R C)
 112    (hRigPrim : PrimitiveRigidityHypotheses R) :
 113    RigidityHypotheses R C := by
 114  refine
 115    { independent_of_state := ?_ }
 116  intro s1 s2 o
 117  exact hPrim.depends_on_ratio (hRigPrim.ratio_state_collapse s1 s2 o)
 118
 119theorem certificate_depends_on_ratio
 120    (R : RatioCostSpace S O) (C : S → O → ℝ)
 121    (h : CertificateHypotheses R C) :
 122    ∀ {s1 s2 : S} {o1 o2 : O},
 123      ratio R s1 o1 = ratio R s2 o2 → C s1 o1 = C s2 o2 :=
 124  h.depends_on_ratio
 125
 126/-- Existence of a reparametrization on the realized cost image.
 127The codomain is `CostCode R` to avoid overclaiming global surjectivity onto `ℝ`. -/
 128theorem exists_monotone_reparam
 129    (R : RatioCostSpace S O) (C : S → O → ℝ)
 130    (h : CertificateHypotheses R C) :
 131    ∃ φ : CostCode R → ℝ,
 132      (∀ s o,
 133          C s o =
 134            φ ⟨canonicalCost R s o, ⟨(s, o), rfl⟩⟩)
 135      ∧
 136      (∀ s o1 o2,
 137          canonicalCost R s o1 ≤ canonicalCost R s o2 →
 138          φ ⟨canonicalCost R s o1, ⟨(s, o1), rfl⟩⟩
 139            ≤
 140          φ ⟨canonicalCost R s o2, ⟨(s, o2), rfl⟩⟩) := by
 141  classical
 142  let φ : CostCode R → ℝ := fun t =>
 143    let p : S × O := Classical.choose t.2
 144    C p.1 p.2
 145  refine ⟨φ, ?_, ?_⟩
 146  · intro s o
 147    let t : CostCode R := ⟨canonicalCost R s o, ⟨(s, o), rfl⟩⟩
 148    have ht :
 149        canonicalCost R (Classical.choose t.2).1 (Classical.choose t.2).2 = t.1 :=
 150      Classical.choose_spec t.2
 151    have hcost :
 152        canonicalCost R s o =
 153          canonicalCost R (Classical.choose t.2).1 (Classical.choose t.2).2 := by
 154      simpa [t] using ht.symm
 155    have hdep :
 156        C s o = C (Classical.choose t.2).1 (Classical.choose t.2).2 :=
 157      h.depends_on_cost hcost
 158    simpa [φ, t] using hdep
 159  · intro s o1 o2 hle
 160    have hrepr1 :
 161        C s o1 = φ ⟨canonicalCost R s o1, ⟨(s, o1), rfl⟩⟩ := by
 162      simpa using (show C s o1 = φ ⟨canonicalCost R s o1, ⟨(s, o1), rfl⟩⟩ from by
 163        let t : CostCode R := ⟨canonicalCost R s o1, ⟨(s, o1), rfl⟩⟩
 164        have ht :
 165            canonicalCost R (Classical.choose t.2).1 (Classical.choose t.2).2 = t.1 :=
 166          Classical.choose_spec t.2
 167        have hcost :
 168            canonicalCost R s o1 =
 169              canonicalCost R (Classical.choose t.2).1 (Classical.choose t.2).2 := by
 170          simpa [t] using ht.symm
 171        have hdep :
 172            C s o1 = C (Classical.choose t.2).1 (Classical.choose t.2).2 :=
 173          h.depends_on_cost hcost
 174        simpa [φ, t] using hdep)
 175    have hrepr2 :
 176        C s o2 = φ ⟨canonicalCost R s o2, ⟨(s, o2), rfl⟩⟩ := by
 177      simpa using (show C s o2 = φ ⟨canonicalCost R s o2, ⟨(s, o2), rfl⟩⟩ from by
 178        let t : CostCode R := ⟨canonicalCost R s o2, ⟨(s, o2), rfl⟩⟩
 179        have ht :
 180            canonicalCost R (Classical.choose t.2).1 (Classical.choose t.2).2 = t.1 :=
 181          Classical.choose_spec t.2
 182        have hcost :
 183            canonicalCost R s o2 =
 184              canonicalCost R (Classical.choose t.2).1 (Classical.choose t.2).2 := by
 185          simpa [t] using ht.symm
 186        have hdep :
 187            C s o2 = C (Classical.choose t.2).1 (Classical.choose t.2).2 :=
 188          h.depends_on_cost hcost
 189        simpa [φ, t] using hdep)
 190    calc
 191      φ ⟨canonicalCost R s o1, ⟨(s, o1), rfl⟩⟩ = C s o1 := by simpa using hrepr1.symm
 192      _ ≤ C s o2 := h.monotone_in_cost s o1 o2 hle
 193      _ = φ ⟨canonicalCost R s o2, ⟨(s, o2), rfl⟩⟩ := by simpa using hrepr2
 194
 195/-- Uniqueness of the realized-cost reparametrization:
 196if a profile `φ` represents all certificate values on `CostCode R`, it is uniquely determined. -/
 197theorem existsUnique_cost_reparam
 198    (R : RatioCostSpace S O) (C : S → O → ℝ)
 199    (h : CertificateHypotheses R C) :
 200    ∃! φ : CostCode R → ℝ, ∀ s o,
 201      C s o = φ ⟨canonicalCost R s o, ⟨(s, o), rfl⟩⟩ := by
 202  rcases exists_monotone_reparam R C h with ⟨φ0, hrepr0, _hmono0⟩
 203  refine ⟨φ0, hrepr0, ?_⟩
 204  intro φ hrepr
 205  funext t
 206  rcases t with ⟨r, hr⟩
 207  rcases hr with ⟨p, hp⟩
 208  rcases p with ⟨s, o⟩
 209  have hcode :
 210      (⟨canonicalCost R s o, ⟨(s, o), rfl⟩⟩ : CostCode R) = ⟨r, ⟨(s, o), hp⟩⟩ := by
 211    apply Subtype.ext
 212    simp [hp]
 213  have hrepr0' : C s o = φ0 ⟨r, ⟨(s, o), hp⟩⟩ := by
 214    simpa [hcode] using hrepr0 s o
 215  have hrepr' : C s o = φ ⟨r, ⟨(s, o), hp⟩⟩ := by
 216    simpa [hcode] using hrepr s o
 217  calc
 218    φ ⟨r, ⟨(s, o), hp⟩⟩ = C s o := by simpa using hrepr'.symm
 219    _ = φ0 ⟨r, ⟨(s, o), hp⟩⟩ := by simpa using hrepr0'
 220
 221/-- Rigidity consequence: if certificate values are state-independent by hypothesis,
 222there exists a single state-free profile `ψ` representing all `C s _`. -/
 223theorem phi_independent_of_state
 224    [Inhabited S]
 225    (R : RatioCostSpace S O) (C : S → O → ℝ)
 226    (hRig : RigidityHypotheses R C) :
 227    ∃ ψ : O → ℝ, ∀ s o, C s o = ψ o := by
 228  refine ⟨fun o => C (default : S) o, ?_⟩
 229  intro s o
 230  exact hRig.independent_of_state s default o
 231
 232/-- Uniqueness of the state-free profile under explicit rigidity:
 233the profile `ψ : O → ℝ` is uniquely determined by certificate values. -/
 234theorem existsUnique_state_profile
 235    [Inhabited S]
 236    (R : RatioCostSpace S O) (C : S → O → ℝ)
 237    (hRig : RigidityHypotheses R C) :
 238    ∃! ψ : O → ℝ, ∀ s o, C s o = ψ o := by
 239  refine ⟨fun o => C (default : S) o, ?_, ?_⟩
 240  · intro s o
 241    exact hRig.independent_of_state s default o
 242  · intro ψ hψ
 243    funext o
 244    exact (hψ default o).symm
 245
 246/-- Assembled forced-factorization statement at the current maximal claim-honest level:
 247cost-image reparametrization + (optional) state-independence under explicit rigidity. -/
 248theorem forced_factorization
 249    [Inhabited S]
 250    (R : RatioCostSpace S O) (C : S → O → ℝ)
 251    (h : CertificateHypotheses R C)
 252    (hRig : RigidityHypotheses R C) :
 253    ∃ φ : CostCode R → ℝ,
 254      (∀ s o,
 255        C s o = φ ⟨canonicalCost R s o, ⟨(s, o), rfl⟩⟩)
 256      ∧
 257      (∃ ψ : O → ℝ, ∀ s o, C s o = ψ o) := by
 258  rcases exists_monotone_reparam R C h with ⟨φ, hrepr, _hmono⟩
 259  rcases phi_independent_of_state R C hRig with ⟨ψ, hψ⟩
 260  exact ⟨φ, hrepr, ⟨ψ, hψ⟩⟩
 261
 262/-- Strongest bundled statement currently proved:
 263both the cost-image reparametrization and the state-free profile are unique
 264under explicit hypothesis bundles. -/
 265theorem forced_factorization_unique
 266    [Inhabited S]
 267    (R : RatioCostSpace S O) (C : S → O → ℝ)
 268    (h : CertificateHypotheses R C)
 269    (hRig : RigidityHypotheses R C) :
 270    (∃! φ : CostCode R → ℝ,
 271      ∀ s o, C s o = φ ⟨canonicalCost R s o, ⟨(s, o), rfl⟩⟩)
 272    ∧
 273    (∃! ψ : O → ℝ, ∀ s o, C s o = ψ o) := by
 274  constructor
 275  · exact existsUnique_cost_reparam R C h
 276  · exact existsUnique_state_profile R C hRig
 277
 278/-- Strong forced-factorization theorem from primitive ratio-level assumptions. -/
 279theorem forced_factorization_unique_of_primitives
 280    [Inhabited S]
 281    (R : RatioCostSpace S O) (C : S → O → ℝ)
 282    (hPrim : PrimitiveCertificateHypotheses R C)
 283    (hRigPrim : PrimitiveRigidityHypotheses R) :
 284    (∃! φ : CostCode R → ℝ,
 285      ∀ s o, C s o = φ ⟨canonicalCost R s o, ⟨(s, o), rfl⟩⟩)
 286    ∧
 287    (∃! ψ : O → ℝ, ∀ s o, C s o = ψ o) := by
 288  exact forced_factorization_unique R C
 289    (primitive_to_certificate R C hPrim)
 290    (primitive_to_rigidity R C hPrim hRigPrim)
 291
 292end ForcedFactorization
 293end CPT
 294end Verification
 295end IndisputableMonolith
 296