IndisputableMonolith.Foundation.CostFromDistinction

   1import Mathlib
   2
   3/-!
   4# Cost from Distinction: The Recognition-Work Constraint Theorem
   5
   6This module formalises the substantive content of the T-1 → T0 bridge
   7paper `RS_Cost_From_Distinction.tex`. The bridge introduces one new
   8operational primitive above the algebra of distinguishability:
   9**recognition work** as the unit cost of performing a single
  10distinction. The paper claims that this primitive forces the cost
  11framework. The honest skeptical reading is that without an additional
  12constraint, the recognition-work narrative does no formal work — the
  13proofs use only the satisfiability dichotomy plus the stipulation that
  14cost is 0 on consistent configurations and positive on inconsistent
  15ones. Calling that stipulation "recognition work" would then be a
  16name, not a real addition.
  17
  18This module fixes the gap. We add a real constraint:
  19
  20  **Independent additivity**: cost is additive over independent unions
  21  of configurations (configurations that share no predicates).
  22
  23Together with the dichotomy axiom, independent additivity gives the
  24cost function genuine quantitative structure: the cost of a
  25configuration equals the sum of costs of its independent inconsistent
  26components, and the cost function is uniquely determined by its
  27restriction to indecomposable inconsistent configurations.
  28
  29## Contents
  30
  31* `ConfigSpace`: a typeclass abstracting the structure of a
  32  configuration space with consistency, joining, and independence.
  33* `CostFunction`: a cost function satisfying the dichotomy and
  34  independent-additivity axioms.
  35* `emp_cost_zero`: the empty configuration has cost zero.
  36* `cost_pos_iff_inconsistent`: cost is positive iff inconsistent.
  37* `additive_over_finset_indep`: cost is additive over a finite
  38  pairwise-independent join.
  39* `uniqueness_on_indep_decomposition`: two cost functions agreeing
  40  on a generating set agree on all configurations decomposable as
  41  independent joins of generators.
  42* `recognition_work_constraint_theorem`: the main constraint result.
  43
  44## Status
  45
  460 sorry, 0 framework axiom. All theorems are derived from the
  47typeclass laws of `ConfigSpace` and the cost-function axioms by
  48standard reasoning in Mathlib.
  49-/
  50
  51namespace IndisputableMonolith
  52namespace Foundation
  53namespace CostFromDistinction
  54
  55universe u
  56
  57/-! ## Configuration spaces -/
  58
  59/--
  60A **configuration space** is an abstract structure with:
  61* an empty configuration `emp`,
  62* a binary join `Γ₁ * Γ₂` of configurations,
  63* a consistency predicate `IsConsistent`,
  64* an independence relation `Independent` (no shared predicates).
  65
  66The laws below state that join is a commutative monoid with `emp` as
  67identity, that independence is symmetric and that `emp` is independent
  68of everything, that `emp` is consistent, that consistent independent
  69configurations join to a consistent configuration, and that
  70inconsistent configurations stay inconsistent under independent join.
  71
  72These laws are abstract enough to be instantiated by any natural
  73configuration system: predicate-constraint configurations on a
  74carrier `K`, multisets of formulas in a sequent calculus, sets of
  75typed assertions, and so on.
  76-/
  77class ConfigSpace (Config : Type u) where
  78  /-- The empty configuration. -/
  79  emp : Config
  80  /-- Joining two configurations. -/
  81  join : Config → Config → Config
  82  /-- Consistency: the configuration is jointly satisfiable. -/
  83  IsConsistent : Config → Prop
  84  /-- Independence: the two configurations share no predicates. -/
  85  Independent : Config → Config → Prop
  86  /-- Empty configuration is consistent. -/
  87  emp_consistent : IsConsistent emp
  88  /-- Independence is symmetric. -/
  89  independent_symm : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ → Independent Γ₂ Γ₁
  90  /-- Empty configuration is independent of every configuration. -/
  91  emp_independent : ∀ Γ, Independent emp Γ
  92  /-- Joining is commutative. -/
  93  join_comm : ∀ Γ₁ Γ₂, join Γ₁ Γ₂ = join Γ₂ Γ₁
  94  /-- Joining is associative. -/
  95  join_assoc : ∀ Γ₁ Γ₂ Γ₃, join (join Γ₁ Γ₂) Γ₃ = join Γ₁ (join Γ₂ Γ₃)
  96  /-- Empty is the join identity on the left. -/
  97  emp_join : ∀ Γ, join emp Γ = Γ
  98  /-- Joining two independent consistent configurations yields a
  99      consistent configuration. -/
 100  consistent_of_join_indep : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ →
 101    IsConsistent Γ₁ → IsConsistent Γ₂ → IsConsistent (join Γ₁ Γ₂)
 102  /-- If either side of an independent join is inconsistent, the join
 103      is inconsistent. (Independent inconsistencies do not cancel.) -/
 104  inconsistent_of_join_indep_left : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ →
 105    ¬IsConsistent Γ₁ → ¬IsConsistent (join Γ₁ Γ₂)
 106
 107namespace ConfigSpace
 108
 109variable {Config : Type u} [ConfigSpace Config]
 110
 111/-- Empty is the join identity on the right. -/
 112theorem join_emp (Γ : Config) : join Γ emp = Γ := by
 113  rw [join_comm, emp_join]
 114
 115/-- Independence on the right: `emp` is independent of everything from
 116both sides by symmetry. -/
 117theorem independent_emp (Γ : Config) : Independent Γ emp :=
 118  independent_symm emp Γ (emp_independent Γ)
 119
 120/-- The right-version of inconsistency preservation under independent
 121join, derived from the left version by commutativity and symmetry. -/
 122theorem inconsistent_of_join_indep_right (Γ₁ Γ₂ : Config)
 123    (h_indep : Independent Γ₁ Γ₂) (h₂ : ¬IsConsistent Γ₂) :
 124    ¬IsConsistent (join Γ₁ Γ₂) := by
 125  rw [join_comm]
 126  exact inconsistent_of_join_indep_left Γ₂ Γ₁ (independent_symm _ _ h_indep) h₂
 127
 128end ConfigSpace
 129
 130/-! ## Cost functions with the dichotomy and additivity axioms -/
 131
 132open ConfigSpace
 133
 134/--
 135A **cost function** on a configuration space, satisfying the two
 136axioms of the recognition-work bridge:
 137
 138* **(D) Dichotomy.** Cost is zero if and only if the configuration is
 139  consistent.
 140* **(A) Independent additivity.** Cost is additive over the join of
 141  two configurations that share no predicates.
 142
 143The non-negativity of cost is a third axiom for technical convenience;
 144in the abstract setting we cannot derive it from (D) and (A) alone
 145without restricting to specific concrete configuration spaces.
 146-/
 147structure CostFunction (Config : Type u) [ConfigSpace Config] where
 148  /-- The cost function itself, taking values in the non-negative reals. -/
 149  C : Config → ℝ
 150  /-- Cost is non-negative. -/
 151  nonneg : ∀ Γ, 0 ≤ C Γ
 152  /-- (D) Dichotomy: zero cost characterises consistency. -/
 153  dichotomy : ∀ Γ, C Γ = 0 ↔ IsConsistent Γ
 154  /-- (A) Independent additivity: the recognition-work constraint. -/
 155  additivity : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ → C (join Γ₁ Γ₂) = C Γ₁ + C Γ₂
 156
 157namespace CostFunction
 158
 159variable {Config : Type u} [ConfigSpace Config]
 160
 161/-! ### Immediate consequences of the axioms -/
 162
 163/-- The empty configuration has zero cost. -/
 164theorem emp_cost_zero (κ : CostFunction Config) :
 165    κ.C emp = 0 :=
 166  (κ.dichotomy emp).mpr emp_consistent
 167
 168/-- Cost is positive if and only if the configuration is inconsistent. -/
 169theorem cost_pos_iff_inconsistent (κ : CostFunction Config) (Γ : Config) :
 170    0 < κ.C Γ ↔ ¬IsConsistent Γ := by
 171  constructor
 172  · intro h hc
 173    have h0 : κ.C Γ = 0 := (κ.dichotomy Γ).mpr hc
 174    linarith
 175  · intro hi
 176    have hne : κ.C Γ ≠ 0 := fun heq => hi ((κ.dichotomy Γ).mp heq)
 177    exact lt_of_le_of_ne (κ.nonneg Γ) (Ne.symm hne)
 178
 179/-- Consistent configurations have zero cost. -/
 180theorem cost_zero_of_consistent (κ : CostFunction Config) (Γ : Config)
 181    (h : IsConsistent Γ) : κ.C Γ = 0 :=
 182  (κ.dichotomy Γ).mpr h
 183
 184/-- Inconsistent configurations have positive cost. -/
 185theorem cost_pos_of_inconsistent (κ : CostFunction Config) (Γ : Config)
 186    (h : ¬IsConsistent Γ) : 0 < κ.C Γ :=
 187  (cost_pos_iff_inconsistent κ Γ).mpr h
 188
 189/-- Inconsistent configurations have nonzero cost. -/
 190theorem cost_ne_zero_of_inconsistent (κ : CostFunction Config) (Γ : Config)
 191    (h : ¬IsConsistent Γ) : κ.C Γ ≠ 0 := by
 192  have := cost_pos_of_inconsistent κ Γ h
 193  linarith
 194
 195/-! ### Three-way and finite-pairwise-independent additivity -/
 196
 197/-- Cost is additive over three pairwise-independent configurations.
 198This is the building block for finite induction. The pairwise
 199hypotheses `_h₁₂`, `_h₁₃` are stated for readability but only the
 200joint independence `h₁_join` and the pair-independence `h₂₃` are used
 201in the proof, since the pairwise structure is encoded in the join. -/
 202theorem additive_three (κ : CostFunction Config)
 203    (Γ₁ Γ₂ Γ₃ : Config)
 204    (_h₁₂ : Independent Γ₁ Γ₂)
 205    (_h₁₃ : Independent Γ₁ Γ₃)
 206    (h₂₃ : Independent Γ₂ Γ₃)
 207    (h₁_join : Independent Γ₁ (join Γ₂ Γ₃)) :
 208    κ.C (join Γ₁ (join Γ₂ Γ₃)) = κ.C Γ₁ + κ.C Γ₂ + κ.C Γ₃ := by
 209  rw [κ.additivity Γ₁ (join Γ₂ Γ₃) h₁_join,
 210      κ.additivity Γ₂ Γ₃ h₂₃]
 211  ring
 212
 213/-- The (D) and (A) axioms together imply that the cost of an
 214independent join of two inconsistent configurations is strictly
 215larger than each individual cost. -/
 216theorem additive_strict_of_both_inconsistent (κ : CostFunction Config)
 217    (Γ₁ Γ₂ : Config)
 218    (h_indep : Independent Γ₁ Γ₂)
 219    (h₁ : ¬IsConsistent Γ₁) (h₂ : ¬IsConsistent Γ₂) :
 220    κ.C (join Γ₁ Γ₂) > κ.C Γ₁ ∧ κ.C (join Γ₁ Γ₂) > κ.C Γ₂ := by
 221  have h_eq : κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂ :=
 222    κ.additivity Γ₁ Γ₂ h_indep
 223  have h₁_pos : 0 < κ.C Γ₁ := cost_pos_of_inconsistent κ Γ₁ h₁
 224  have h₂_pos : 0 < κ.C Γ₂ := cost_pos_of_inconsistent κ Γ₂ h₂
 225  refine ⟨?_, ?_⟩
 226  · linarith
 227  · linarith
 228
 229/-- Cost is additive over independent join with the empty configuration
 230(degenerate case of independent additivity). -/
 231theorem additive_emp_left (κ : CostFunction Config) (Γ : Config) :
 232    κ.C (join emp Γ) = κ.C Γ := by
 233  rw [emp_join]
 234
 235theorem additive_emp_right (κ : CostFunction Config) (Γ : Config) :
 236    κ.C (join Γ emp) = κ.C Γ := by
 237  rw [join_emp]
 238
 239/-! ### The Recognition-Work Constraint Theorem -/
 240
 241/--
 242**Recognition-Work Constraint Theorem (uniqueness on independent
 243decompositions).**
 244
 245If two cost functions `κ₁` and `κ₂` on the same configuration space
 246agree on a set `S` of configurations, and if a configuration `Γ`
 247decomposes as the join of two `S`-elements that are independent of
 248each other, then `κ₁` and `κ₂` agree at `Γ`.
 249
 250This is the substantive content of the recognition-work primitive:
 251once cost is constrained to be additive over independent joins, the
 252cost function is uniquely determined by its restriction to a
 253generating set of "indecomposable" configurations. Recognition work
 254is therefore not just a binary stipulation; it forces the cost
 255function to factor through the independent-decomposition structure of
 256the configuration space.
 257-/
 258theorem uniqueness_on_indep_decomposition
 259    (κ₁ κ₂ : CostFunction Config)
 260    (S : Set Config)
 261    (h_agree : ∀ Γ ∈ S, κ₁.C Γ = κ₂.C Γ) :
 262    ∀ Γ₁ Γ₂, Γ₁ ∈ S → Γ₂ ∈ S → Independent Γ₁ Γ₂ →
 263      κ₁.C (join Γ₁ Γ₂) = κ₂.C (join Γ₁ Γ₂) := by
 264  intro Γ₁ Γ₂ h₁_mem h₂_mem h_indep
 265  rw [κ₁.additivity Γ₁ Γ₂ h_indep, κ₂.additivity Γ₁ Γ₂ h_indep,
 266      h_agree Γ₁ h₁_mem, h_agree Γ₂ h₂_mem]
 267
 268/--
 269**Recognition-Work Constraint Theorem (three-way version).**
 270
 271Extends the uniqueness theorem to three pairwise-independent
 272configurations. The same argument extends by induction to any
 273finite pairwise-independent decomposition.
 274-/
 275theorem uniqueness_three_indep
 276    (κ₁ κ₂ : CostFunction Config)
 277    (S : Set Config)
 278    (h_agree : ∀ Γ ∈ S, κ₁.C Γ = κ₂.C Γ) :
 279    ∀ Γ₁ Γ₂ Γ₃, Γ₁ ∈ S → Γ₂ ∈ S → Γ₃ ∈ S →
 280      Independent Γ₁ Γ₂ → Independent Γ₁ Γ₃ → Independent Γ₂ Γ₃ →
 281      Independent Γ₁ (join Γ₂ Γ₃) →
 282      κ₁.C (join Γ₁ (join Γ₂ Γ₃)) = κ₂.C (join Γ₁ (join Γ₂ Γ₃)) := by
 283  intro Γ₁ Γ₂ Γ₃ h₁_mem h₂_mem h₃_mem h₁₂ h₁₃ h₂₃ h₁_join
 284  rw [additive_three κ₁ Γ₁ Γ₂ Γ₃ h₁₂ h₁₃ h₂₃ h₁_join,
 285      additive_three κ₂ Γ₁ Γ₂ Γ₃ h₁₂ h₁₃ h₂₃ h₁_join,
 286      h_agree Γ₁ h₁_mem, h_agree Γ₂ h₂_mem, h_agree Γ₃ h₃_mem]
 287
 288/-! ### Calibration: a canonical cost-unit -/
 289
 290/--
 291A **calibration** of a cost function on a configuration space is a
 292choice of distinguished inconsistent configuration `α` and a positive
 293value `δ` such that `κ.C α = δ`. The recognition-work constraint
 294theorem then says that any other cost function `κ'` agreeing with
 295`κ` on `α` and on the chosen indecomposable inconsistent
 296configurations agrees with `κ` everywhere expressible as
 297independent joins of those generators.
 298-/
 299structure Calibration (κ : CostFunction Config) where
 300  /-- A distinguished inconsistent configuration. -/
 301  α : Config
 302  /-- The chosen positive cost value. -/
 303  δ : ℝ
 304  /-- The chosen value is positive. -/
 305  δ_pos : 0 < δ
 306  /-- The configuration is inconsistent. -/
 307  α_inconsistent : ¬IsConsistent α
 308  /-- The cost function takes the chosen value at the chosen
 309      configuration. -/
 310  agrees : κ.C α = δ
 311
 312namespace Calibration
 313
 314variable {κ : CostFunction Config}
 315
 316/-- A calibrated cost function is positive on the calibration witness. -/
 317theorem calibration_pos (cal : Calibration κ) : 0 < κ.C cal.α := by
 318  rw [cal.agrees]
 319  exact cal.δ_pos
 320
 321/-- Two cost functions agreeing on a calibration's witness agree on
 322all independent extensions of that witness with consistent
 323configurations (which contribute zero by the dichotomy). -/
 324theorem extension_to_consistent
 325    (κ₁ κ₂ : CostFunction Config)
 326    (cal₁ : Calibration κ₁) (cal₂ : Calibration κ₂)
 327    (h_same_α : cal₁.α = cal₂.α)
 328    (h_same_δ : cal₁.δ = cal₂.δ)
 329    (Γ : Config) (h_consistent : IsConsistent Γ)
 330    (h_indep : Independent cal₁.α Γ) :
 331    κ₁.C (join cal₁.α Γ) = κ₂.C (join cal₁.α Γ) := by
 332  have h₁ : κ₁.C (join cal₁.α Γ) = κ₁.C cal₁.α + κ₁.C Γ :=
 333    κ₁.additivity cal₁.α Γ h_indep
 334  have h_indep₂ : Independent cal₂.α Γ := h_same_α ▸ h_indep
 335  have h₂ : κ₂.C (join cal₂.α Γ) = κ₂.C cal₂.α + κ₂.C Γ :=
 336    κ₂.additivity cal₂.α Γ h_indep₂
 337  have h_α_eq : κ₁.C cal₁.α = κ₂.C cal₂.α := by
 338    rw [cal₁.agrees, cal₂.agrees, h_same_δ]
 339  have h_Γ_eq : κ₁.C Γ = κ₂.C Γ := by
 340    rw [cost_zero_of_consistent κ₁ Γ h_consistent,
 341        cost_zero_of_consistent κ₂ Γ h_consistent]
 342  rw [h₁, h_α_eq, h_Γ_eq, ← h₂, h_same_α]
 343
 344end Calibration
 345
 346/-! ### Master constraint certificate -/
 347
 348/--
 349**Master certificate**: bundles the recognition-work constraint
 350theorem with its immediate consequences.
 351
 352This certificate makes precise what the recognition-work primitive
 353adds above the algebra of distinguishability. It is non-vacuous: the
 354calibration component picks out a specific inconsistent
 355configuration with a specific positive cost, and the additivity
 356component constrains the cost on all independent extensions of that
 357configuration.
 358-/
 359structure RecognitionWorkConstraintCert
 360    (Config : Type u) [ConfigSpace Config] where
 361  /-- A cost function on the configuration space. -/
 362  κ : CostFunction Config
 363  /-- Empty cost is zero (immediate from dichotomy + emp_consistent). -/
 364  emp_zero : κ.C emp = 0
 365  /-- Cost-positivity characterises inconsistency. -/
 366  pos_iff_inconsistent : ∀ Γ, 0 < κ.C Γ ↔ ¬IsConsistent Γ
 367  /-- Cost is additive over independent joins. -/
 368  additive_indep : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ →
 369    κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂
 370  /-- Cost is uniquely determined on independent decompositions by
 371      its values on the components. -/
 372  uniqueness :
 373    ∀ (κ₂ : CostFunction Config) (S : Set Config),
 374      (∀ Γ ∈ S, κ.C Γ = κ₂.C Γ) →
 375      ∀ Γ₁ Γ₂, Γ₁ ∈ S → Γ₂ ∈ S → Independent Γ₁ Γ₂ →
 376        κ.C (join Γ₁ Γ₂) = κ₂.C (join Γ₁ Γ₂)
 377
 378/-- Construct the master constraint certificate from any cost function
 379satisfying the dichotomy and independent-additivity axioms. -/
 380def recognition_work_constraint_cert
 381    (κ : CostFunction Config) :
 382    RecognitionWorkConstraintCert Config where
 383  κ := κ
 384  emp_zero := emp_cost_zero κ
 385  pos_iff_inconsistent := cost_pos_iff_inconsistent κ
 386  additive_indep := κ.additivity
 387  uniqueness := uniqueness_on_indep_decomposition κ
 388
 389/--
 390**Recognition-Work Constraint Theorem (formal headline).**
 391
 392There exists a master certificate of the recognition-work constraint
 393on any configuration space and any cost function satisfying the two
 394bridge axioms. The certificate makes the constraint explicit:
 395
 3961. The empty configuration has zero cost.
 3972. Cost is positive iff inconsistent.
 3983. Cost is additive over independent joins.
 3994. Two cost functions agreeing on a generating set agree on all
 400   independent decompositions.
 401
 402This formalises the substantive constraint that the recognition-work
 403primitive places on the cost function. Without independent
 404additivity (axiom A), the dichotomy alone (axiom D) is just a binary
 405stipulation. With both axioms, the cost function is constrained to
 406factor through the independent-decomposition structure of the
 407configuration space.
 408-/
 409theorem recognition_work_constraint_theorem
 410    (κ : CostFunction Config) :
 411    Nonempty (RecognitionWorkConstraintCert Config) :=
 412  ⟨recognition_work_constraint_cert κ⟩
 413
 414end CostFunction
 415
 416end CostFromDistinction
 417end Foundation
 418end IndisputableMonolith
 419