IndisputableMonolith.Foundation.RecognitionLedgerFloor

   1import Mathlib
   2import IndisputableMonolith.Foundation.CostFromDistinction
   3
   4/-!
   5# Recognition Ledger Floor: the free additive cost floor
   6
   7This module closes the two genuine mathematical gaps identified in the
   8T-1 / T0 audit (the "Anil" critique, May 2026), as opposed to the many
   9"loopholes" that merely restate that a two-state floor is minimal.
  10
  11The two real gaps are dual:
  12
  13* the **kernel gap** (audit Loophole 2): the observable equivalence should be
  14  *derived* from the cost functional (its kernel), not imposed as an external
  15  setoid or a gauge group;
  16* the **cokernel gap** (audit Loophole 9): independent defects should
  17  *accumulate additively with multiplicity*, instead of being excluded from the
  18  independence relation to dodge `1 = 2` (audit Loophole 8).
  19
  20Both are answered by one object: the free commutative monoid on a type `I` of
  21primitive distinctions,
  22
  23```
  24DefectLedger I := I →₀ ℕ,
  25```
  26
  27with cost `ledgerCost w` for a strictly positive weight `w`. On this carrier:
  28
  29* additivity is **unconditional** (`ledgerCost_add`); no restricted independence
  30  relation is needed, so the `(true, true)` evasion of the Boolean floor
  31  disappears;
  32* the observable equivalence is the **kernel** of the cost (`observableSetoid`),
  33  and the floor is non-vacuous exactly when some weight is positive
  34  (`observable_floor_iff_pos_weight`);
  35* two independent copies of the same defect genuinely cost `2 w i`
  36  (`two_independent_same_defects`), i.e. multiplicity is represented;
  37* the data assembles into the existing `CostFromDistinction.CostFunction`
  38  abstraction with the **universal** independence relation
  39  (`ledgerConfigSpace`, `ledgerCostFunction`).
  40
  41The two-state Boolean floor of T0 is the `n ∈ {0,1}` truncation of this object
  42under unit weight (`boolean_floor_is_truncation`).
  43
  44Status: 0 sorry, 0 new axiom.
  45-/
  46
  47namespace IndisputableMonolith
  48namespace Foundation
  49namespace RecognitionLedgerFloor
  50
  51open CostFromDistinction
  52
  53universe u
  54variable {I : Type u}
  55
  56/-- A defect ledger: finitely supported multiplicities of primitive
  57distinctions. This is the free commutative monoid on `I`. -/
  58abbrev DefectLedger (I : Type u) := I →₀ ℕ
  59
  60/-- Recognition cost of a ledger under a per-distinction weight `w`: the total
  61weighted multiplicity of performed distinctions. -/
  62noncomputable def ledgerCost (w : I → ℝ) (Γ : DefectLedger I) : ℝ :=
  63  Γ.sum (fun i n => (n : ℝ) * w i)
  64
  65@[simp] theorem ledgerCost_zero (w : I → ℝ) :
  66    ledgerCost w (0 : DefectLedger I) = 0 := by
  67  simp [ledgerCost]
  68
  69/-- **Unconditional additivity.** The free ledger needs no restriction of the
  70independence relation: the cost of a sum is always the sum of the costs. -/
  71theorem ledgerCost_add (w : I → ℝ) (Γ Δ : DefectLedger I) :
  72    ledgerCost w (Γ + Δ) = ledgerCost w Γ + ledgerCost w Δ := by
  73  unfold ledgerCost
  74  refine Finsupp.sum_add_index' ?_ ?_
  75  · intro i; simp
  76  · intro i a b; push_cast; ring
  77
  78/-- The cost of a single defect of multiplicity `n` is `n · w i`. -/
  79theorem ledgerCost_single (w : I → ℝ) (i : I) (n : ℕ) :
  80    ledgerCost w (Finsupp.single i n) = (n : ℝ) * w i := by
  81  unfold ledgerCost
  82  rw [Finsupp.sum_single_index (by simp)]
  83
  84theorem ledgerCost_nonneg (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) (Γ : DefectLedger I) :
  85    0 ≤ ledgerCost w Γ := by
  86  unfold ledgerCost
  87  refine Finset.sum_nonneg ?_
  88  intro i _
  89  exact mul_nonneg (Nat.cast_nonneg _) (hw i)
  90
  91/-! ## The observable quotient is the kernel of the cost (closes Loophole 2) -/
  92
  93/-- Two ledgers are observationally the same when no weighted recognition cost
  94separates them. This is the *kernel* of the cost functional: the equivalence is
  95derived from cost, not imposed externally. -/
  96def ObservablySame (w : I → ℝ) (Γ Δ : DefectLedger I) : Prop :=
  97  ledgerCost w Γ = ledgerCost w Δ
  98
  99/-- The observable equivalence relation generated by the cost functional. -/
 100def observableSetoid (w : I → ℝ) : Setoid (DefectLedger I) where
 101  r := ObservablySame w
 102  iseqv := ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => h₁.trans h₂⟩
 103
 104/-- Cost is, by construction, constant on observable classes. Gauge invariance
 105is therefore automatic rather than assumed. -/
 106theorem ledgerCost_constant_on_classes (w : I → ℝ) {Γ Δ : DefectLedger I}
 107    (h : (observableSetoid w).r Γ Δ) : ledgerCost w Γ = ledgerCost w Δ := h
 108
 109/-- **Non-vacuity of the observable floor.** The cost kernel is proper (there
 110exist observably distinct ledgers) exactly when some distinction carries
 111positive weight. With a constant-zero weight the kernel is everything, which is
 112the correct RS reading of the indiscrete gauge counterexample. -/
 113theorem observable_floor_iff_pos_weight (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) :
 114    (∃ Γ Δ : DefectLedger I, ¬ ObservablySame w Γ Δ) ↔ (∃ i, 0 < w i) := by
 115  constructor
 116  · rintro ⟨Γ, Δ, hne⟩
 117    by_contra hno
 118    push_neg at hno
 119    have hzero : ∀ i, w i = 0 := fun i => le_antisymm (hno i) (hw i)
 120    apply hne
 121    show ledgerCost w Γ = ledgerCost w Δ
 122    have hall : ∀ Θ : DefectLedger I, ledgerCost w Θ = 0 := by
 123      intro Θ
 124      unfold ledgerCost
 125      refine Finset.sum_eq_zero ?_
 126      intro i _
 127      simp [hzero i]
 128    rw [hall Γ, hall Δ]
 129  · rintro ⟨i, hi⟩
 130    refine ⟨Finsupp.single i 1, 0, ?_⟩
 131    intro hsame
 132    have h : ledgerCost w (Finsupp.single i 1) = ledgerCost w (0 : DefectLedger I) := hsame
 133    rw [ledgerCost_single, ledgerCost_zero] at h
 134    push_cast at h
 135    simp only [one_mul] at h
 136    exact hi.ne' h
 137
 138/-! ## Strict positivity gives the dichotomy (consistency = zero cost) -/
 139
 140/-- With strictly positive weights, a ledger is costless exactly when it is the
 141empty ledger. This is the recognition-work dichotomy on the free floor. -/
 142theorem ledgerCost_eq_zero_iff (w : I → ℝ) (hw : ∀ i, 0 < w i)
 143    (Γ : DefectLedger I) :
 144    ledgerCost w Γ = 0 ↔ Γ = 0 := by
 145  constructor
 146  · intro h
 147    by_contra hΓ
 148    have hne : Γ.support.Nonempty := Finsupp.support_nonempty_iff.mpr hΓ
 149    obtain ⟨i, hi_supp⟩ := hne
 150    have hi : Γ i ≠ 0 := Finsupp.mem_support_iff.mp hi_supp
 151    have hpos : 0 < (Γ i : ℝ) * w i :=
 152      mul_pos (by exact_mod_cast Nat.pos_of_ne_zero hi) (hw i)
 153    have hnonneg : ∀ j ∈ Γ.support, 0 ≤ (Γ j : ℝ) * w j :=
 154      fun j _ => mul_nonneg (Nat.cast_nonneg _) (le_of_lt (hw j))
 155    have hle : (Γ i : ℝ) * w i ≤ ledgerCost w Γ :=
 156      Finset.single_le_sum hnonneg hi_supp
 157    linarith
 158  · intro h; subst h; simp
 159
 160/-! ## Multiplicity is represented (closes Loopholes 8 and 9) -/
 161
 162/-- **The cokernel fix.** Two independent copies of the same defect cost `2 w i`,
 163not `w i`. Multiplicity is genuinely represented, so the free ledger needs no
 164restriction of independence to avoid `1 = 2`: on this carrier, `1 + 1 = 2`. -/
 165theorem two_independent_same_defects (w : I → ℝ) (i : I) :
 166    ledgerCost w (Finsupp.single i 1 + Finsupp.single i 1) = 2 * w i := by
 167  rw [ledgerCost_add, ledgerCost_single]
 168  push_cast
 169  ring
 170
 171/-- The Boolean two-state floor of T0 is the unit-weight truncation of the
 172ledger: cost equals multiplicity, and the Boolean floor is the clamp to
 173`{0, 1}`. -/
 174theorem boolean_floor_is_truncation (i : I) (n : ℕ) :
 175    ledgerCost (fun _ => (1 : ℝ)) (Finsupp.single i n) = (n : ℝ) := by
 176  rw [ledgerCost_single]; ring
 177
 178/-- Boolean shadow of a natural-number generator count: zero is `false`, any
 179positive multiplicity is `true`. -/
 180def booleanTruncation (n : ℕ) : Bool :=
 181  decide (n ≠ 0)
 182
 183@[simp] theorem booleanTruncation_zero :
 184    booleanTruncation 0 = false := by
 185  simp [booleanTruncation]
 186
 187@[simp] theorem booleanTruncation_pos {n : ℕ} (hn : n ≠ 0) :
 188    booleanTruncation n = true := by
 189  simp [booleanTruncation, hn]
 190
 191/-- OR on the Boolean T0 floor is induced by adding generator counts and then
 192truncating back to `{0, 1}`. -/
 193theorem booleanTruncation_add_eq_or (m n : ℕ) :
 194    booleanTruncation (m + n) =
 195      (booleanTruncation m || booleanTruncation n) := by
 196  unfold booleanTruncation
 197  by_cases hm : m = 0
 198  · subst m
 199    simp
 200  · by_cases hn : n = 0
 201    · subst n
 202      simp [hm]
 203    · have hsum : m + n ≠ 0 := by omega
 204      simp [hm, hn]
 205
 206/-- Under unit weight, the ledger cost of `n` copies of one primitive
 207distinction is exactly the natural-number generator count. -/
 208theorem unit_cost_is_generator_count (i : I) (n : ℕ) :
 209    ledgerCost (fun _ => (1 : ℝ)) (Finsupp.single i n) = (n : ℝ) :=
 210  boolean_floor_is_truncation i n
 211
 212/-! ## Assembly into the existing `CostFunction` abstraction
 213
 214The free ledger instantiates `CostFromDistinction.ConfigSpace` with the
 215**universal** independence relation (every pair independent), and yet supports a
 216genuine `CostFunction`. This is the concrete refutation of audit Loophole 8: the
 217independence relation is not gerrymandered to avoid `1 = 2`; multiplicity makes
 218universal independence consistent with additivity. -/
 219
 220/-- The free ledger as a configuration space, with universal independence. -/
 221noncomputable instance ledgerConfigSpace : ConfigSpace (DefectLedger I) where
 222  emp := 0
 223  join := (· + ·)
 224  IsConsistent := fun Γ => Γ = 0
 225  Independent := fun _ _ => True
 226  emp_consistent := rfl
 227  independent_symm := fun _ _ _ => trivial
 228  emp_independent := fun _ => trivial
 229  join_comm := add_comm
 230  join_assoc := fun a b c => add_assoc a b c
 231  emp_join := zero_add
 232  consistent_of_join_indep := by
 233    intro Γ₁ Γ₂ _ h₁ h₂
 234    subst h₁; subst h₂; simp
 235  inconsistent_of_join_indep_left := by
 236    intro Γ₁ Γ₂ _ h₁ hsum
 237    have hsum' : Γ₁ + Γ₂ = 0 := hsum
 238    apply h₁
 239    ext i
 240    have hi : Γ₁ i + Γ₂ i = 0 := by
 241      have h := congrArg (fun f : DefectLedger I => f i) hsum'
 242      simpa [Finsupp.add_apply] using h
 243    have h0 : Γ₁ i = 0 := by omega
 244    simpa using h0
 245
 246/-- The free ledger carries a genuine recognition-work `CostFunction` for any
 247strictly positive weight, with universal independence. -/
 248noncomputable def ledgerCostFunction (w : I → ℝ) (hw : ∀ i, 0 < w i) :
 249    CostFunction (DefectLedger I) where
 250  C := ledgerCost w
 251  nonneg := ledgerCost_nonneg w (fun i => le_of_lt (hw i))
 252  dichotomy := by
 253    intro Γ
 254    exact ledgerCost_eq_zero_iff w hw Γ
 255  additivity := by
 256    intro Γ₁ Γ₂ _
 257    exact ledgerCost_add w Γ₁ Γ₂
 258
 259/-- The free ledger satisfies the recognition-work constraint theorem of
 260`CostFromDistinction`, with multiplicity represented and independence universal. -/
 261theorem ledger_recognition_work_constraint (w : I → ℝ) (hw : ∀ i, 0 < w i) :
 262    Nonempty (CostFunction.RecognitionWorkConstraintCert (DefectLedger I)) :=
 263  CostFunction.recognition_work_constraint_theorem (ledgerCostFunction w hw)
 264
 265end RecognitionLedgerFloor
 266end Foundation
 267end IndisputableMonolith
 268