IndisputableMonolith.Cosmology.GradedRungCost

   1import Mathlib
   2import IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCost
   3
   4/-!
   5# The graded-rung cost ledger: any unit-step phi-rung field pays J(phi) per forced distinction
   6
   7Phase 55 (`PolarizedBirthInterfaceCost`) proved the recognition-cost ledger for the *binary* birth
   8field, whose charge is `sign(x) in {+1, 0, -1}`: carried bulk costs zero, the interface costs
   9`(count) * J(phi)`. But the live engine carries a *graded* phi-rung profile, not a single sign flip:
  10the north star is to "carry each region at the coarsest phi-rung its recognition allows," which is a
  11multi-valued rung field. This module proves the cost law at that level of generality.
  12
  13The only property the cost law needs is the **forced minimal-distinction property**: across every
  14adjacency the rung changes by at most one (`UnitStep`). A unit recognition step resolves at most one
  15phi-rung, so `k p - k q in {0, +1, -1}` for every edge `(p, q)`. This is exactly what the lattice
  16plus the single-rung-step law forces (it is the `level_diff` mechanism of Phase 55), and it is the
  17invariant the live engine maintains because the T-3 refiner descends one rung at a time.
  18
  19For **any** finite ordered edge set `E : Finset (V x V)` and **any** integer rung field `k : V -> Z`
  20satisfying `UnitStep k E`, this module proves, over the reals with 0 `sorry` and only the three
  21standard axioms (`propext`, `Classical.choice`, `Quot.sound`):
  22
  23* a carried (equal-rung) adjacency costs exactly `0` (`edgeCost_carried`): `J(phi^0) = J(1) = 0`;
  24* an interface (different-rung) adjacency costs exactly `J(phi)` (`edgeCost_interface`): the gap is
  25  forced to `±1` rung, so `J(phi^(±1)) = J(phi)` by reciprocal symmetry;
  26* `carriedCost = 0` (`carriedCost_eq_zero`), `totalCost = interfaceCost`
  27  (`totalCost_eq_interfaceCost`), and the closed form `totalCost = (interface edge count) * J(phi)`
  28  (`totalCost_eq_card`), with `J(phi) > 0` (`Jcost_phi_pos`).
  29
  30So the engine pays exactly `J(phi)` per forced unit-rung distinction and carries the entire same-rung
  31bulk for free, for *any* rung profile, not just the binary birth field. The polarized birth field of
  32Phase 55 is recovered as the `k = polarized` special case (`Diamond.polarized_totalCost_card`,
  33`Octahedron.polarized_totalCost_card`), with `UnitStep` discharged by the Phase-55 `level_diff`
  34(`Diamond.polarized_unitStep`, `Octahedron.polarized_unitStep`).
  35
  36THEOREM (0 `sorry`, standard three axioms only). The `UnitStep` hypothesis is the forced
  37minimal-distinction property, proved here for the birth field and maintained by the engine's T-3
  38single-rung refinement; it is not a fitted parameter.
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Cosmology
  43namespace GradedRungCost
  44
  45open Finset
  46open scoped BigOperators
  47open PolarizedBirthInterfaceCost (Jpow Jpow_zero Jpow_of_abs_one Jcost_phi_pos)
  48
  49variable {V : Type*}
  50
  51/-! ## §1. The per-edge cost and the forced minimal-distinction property -/
  52
  53/-- The recognition cost of one ordered adjacency `(p.1, p.2)` under a phi-rung field `k`:
  54`J(phi^(k p.1 - k p.2))`, the forced cost `J` evaluated at the rung gap. -/
  55noncomputable def edgeCost (k : V → ℤ) (p : V × V) : ℝ := Jpow (k p.1 - k p.2)
  56
  57/-- **The forced minimal-distinction property.** A rung field `k` posts only single-rung distinctions
  58across the edge set `E`: every adjacency changes the rung by at most one, `k p.1 - k p.2 in {0,+1,-1}`.
  59A unit recognition step resolves at most one phi-rung; the live engine maintains this because T-3
  60descends one rung at a time. -/
  61def UnitStep (k : V → ℤ) (E : Finset (V × V)) : Prop :=
  62  ∀ p ∈ E, k p.1 - k p.2 = 0 ∨ k p.1 - k p.2 = 1 ∨ k p.1 - k p.2 = -1
  63
  64/-- A carried (equal-rung) adjacency costs exactly zero: `J(phi^0) = J(1) = 0`. -/
  65theorem edgeCost_carried (k : V → ℤ) {p : V × V} (h : k p.1 = k p.2) :
  66    edgeCost k p = 0 := by
  67  have hz : k p.1 - k p.2 = 0 := sub_eq_zero.mpr h
  68  rw [edgeCost, hz, Jpow_zero]
  69
  70/-- Under the unit-step law, an interface (different-rung) adjacency costs exactly `J(phi)`: the gap
  71is forced to `±1` rung, and `J(phi^(±1)) = J(phi)` by reciprocal symmetry. -/
  72theorem edgeCost_interface (k : V → ℤ) {E : Finset (V × V)} (hk : UnitStep k E)
  73    {p : V × V} (hp : p ∈ E) (hne : k p.1 ≠ k p.2) :
  74    edgeCost k p = Cost.Jcost Constants.phi := by
  75  have hd : k p.1 - k p.2 = 1 ∨ k p.1 - k p.2 = -1 := by
  76    rcases hk p hp with h0 | h1 | hm1
  77    · exact absurd (sub_eq_zero.mp h0) hne
  78    · exact Or.inl h1
  79    · exact Or.inr hm1
  80  rw [edgeCost]
  81  exact Jpow_of_abs_one hd
  82
  83/-! ## §2. The three ledger sums and the closed form -/
  84
  85/-- The total interface recognition cost: the sum of `edgeCost` over the different-rung edges. -/
  86noncomputable def interfaceCost (k : V → ℤ) (E : Finset (V × V)) : ℝ :=
  87  ∑ p ∈ E.filter (fun p => k p.1 ≠ k p.2), edgeCost k p
  88
  89/-- The total carried recognition cost: the sum of `edgeCost` over the equal-rung edges. -/
  90noncomputable def carriedCost (k : V → ℤ) (E : Finset (V × V)) : ℝ :=
  91  ∑ p ∈ E.filter (fun p => k p.1 = k p.2), edgeCost k p
  92
  93/-- The total recognition cost of the field: the sum of `edgeCost` over every adjacency. -/
  94noncomputable def totalCost (k : V → ℤ) (E : Finset (V × V)) : ℝ :=
  95  ∑ p ∈ E, edgeCost k p
  96
  97/-- **Carried cost is exactly zero.** The whole same-rung bulk the engine carries coarse is free. -/
  98theorem carriedCost_eq_zero (k : V → ℤ) (E : Finset (V × V)) :
  99    carriedCost k E = 0 := by
 100  simp only [carriedCost]
 101  apply Finset.sum_eq_zero
 102  intro p hp
 103  rw [Finset.mem_filter] at hp
 104  exact edgeCost_carried k hp.2
 105
 106/-- **The total cost equals the interface cost**, because the carried bulk contributes nothing. -/
 107theorem totalCost_eq_interfaceCost (k : V → ℤ) (E : Finset (V × V)) :
 108    totalCost k E = interfaceCost k E := by
 109  have hsplit := Finset.sum_filter_add_sum_filter_not E (fun p => k p.1 ≠ k p.2) (edgeCost k)
 110  have hzero : ∑ p ∈ E.filter (fun p => ¬ (k p.1 ≠ k p.2)), edgeCost k p = 0 := by
 111    apply Finset.sum_eq_zero
 112    intro p hp
 113    rw [Finset.mem_filter] at hp
 114    exact edgeCost_carried k (not_not.mp hp.2)
 115  rw [hzero, add_zero] at hsplit
 116  simp only [totalCost, interfaceCost]
 117  exact hsplit.symm
 118
 119/-- The interface cost is the interface edge count times `J(phi)` (`UnitStep` makes every
 120different-rung edge cost exactly one `J(phi)`). -/
 121theorem interfaceCost_eq_card (k : V → ℤ) (E : Finset (V × V)) (hk : UnitStep k E) :
 122    interfaceCost k E = (E.filter (fun p => k p.1 ≠ k p.2)).card • Cost.Jcost Constants.phi := by
 123  have hpt : ∀ p ∈ E.filter (fun p => k p.1 ≠ k p.2),
 124      edgeCost k p = Cost.Jcost Constants.phi := by
 125    intro p hp
 126    rw [Finset.mem_filter] at hp
 127    exact edgeCost_interface k hk hp.1 hp.2
 128  simp only [interfaceCost]
 129  rw [Finset.sum_congr rfl hpt, Finset.sum_const]
 130
 131/-- **The total recognition cost of any unit-step rung field is `(interface edge count) * J(phi)`.**
 132Carried bulk is free; the whole cost sits on the forced unit-rung distinctions. -/
 133theorem totalCost_eq_card (k : V → ℤ) (E : Finset (V × V)) (hk : UnitStep k E) :
 134    totalCost k E = (E.filter (fun p => k p.1 ≠ k p.2)).card • Cost.Jcost Constants.phi := by
 135  rw [totalCost_eq_interfaceCost, interfaceCost_eq_card k E hk]
 136
 137/-- **Graded-rung cost ledger headline (Phase 56).** For any finite ordered edge set `E` and any
 138integer rung field `k` with the forced minimal-distinction property `UnitStep k E`: the carried
 139same-rung bulk costs exactly zero, the total cost equals the interface cost, the total cost is the
 140interface edge count times the one-rung cost `J(phi)`, and `J(phi) > 0` is a genuine positive cost.
 141The cost of carrying any rung profile is `J(phi)` per forced unit-rung distinction, bulk free. -/
 142theorem t56_graded_cost_ledger (k : V → ℤ) (E : Finset (V × V)) (hk : UnitStep k E) :
 143    carriedCost k E = 0
 144    ∧ totalCost k E = interfaceCost k E
 145    ∧ totalCost k E = (E.filter (fun p => k p.1 ≠ k p.2)).card • Cost.Jcost Constants.phi
 146    ∧ 0 < Cost.Jcost Constants.phi :=
 147  ⟨carriedCost_eq_zero k E, totalCost_eq_interfaceCost k E,
 148   totalCost_eq_card k E hk, Jcost_phi_pos⟩
 149
 150/-! ## §3. The polarized birth field is the `k = sign(x)` special case (2D) -/
 151
 152namespace Diamond
 153
 154open InterfaceComponentBound.Diamond
 155open PolarizedBirthDomains.Diamond (polarized)
 156open LatticeBallEdges.Diamond (E)
 157
 158/-- **The polarized birth field satisfies the forced minimal-distinction property.** Every adjacency
 159of the diamond either keeps the charge (carried, gap `0`) or flips it across the spine, and the
 160Phase-55 `level_diff` shows a flip is exactly `±1` rung. So `UnitStep (polarized t) (E t)`. -/
 161theorem polarized_unitStep (t : ℕ) : UnitStep (polarized t) (E t) := by
 162  intro p hp
 163  rw [E, Finset.mem_filter] at hp
 164  by_cases h : polarized t p.1 = polarized t p.2
 165  · exact Or.inl (sub_eq_zero.mpr h)
 166  · rcases PolarizedBirthInterfaceCost.Diamond.level_diff t p.1 p.2 hp.2 h with h1 | hm1
 167    · exact Or.inr (Or.inl h1)
 168    · exact Or.inr (Or.inr hm1)
 169
 170/-- The general graded-rung `totalCost` at `k = polarized t` is definitionally the Phase-55
 171`PolarizedBirthInterfaceCost.Diamond.totalCost t`. -/
 172theorem polarized_totalCost (t : ℕ) :
 173    totalCost (polarized t) (E t) = PolarizedBirthInterfaceCost.Diamond.totalCost t := rfl
 174
 175/-- **The general law recovers the Phase-55 2D closed form.** Instantiating the graded-rung ledger at
 176the polarized birth field gives `totalCost = (8t - 4) * J(phi)` (`t >= 1`): Phase 55 is the binary
 177special case of the graded-rung cost law. -/
 178theorem polarized_totalCost_card (t : ℕ) (ht : 1 ≤ t) :
 179    totalCost (polarized t) (E t) = (8 * t - 4) • Cost.Jcost Constants.phi := by
 180  rw [polarized_totalCost, PolarizedBirthInterfaceCost.Diamond.totalCost_card t ht]
 181
 182end Diamond
 183
 184/-! ## §4. The polarized birth field is the `k = sign(x)` special case (3D) -/
 185
 186namespace Octahedron
 187
 188open InterfaceComponentBound.Octahedron
 189open PolarizedBirthDomains.Octahedron (polarized)
 190open LatticeBallEdges.Octahedron (E)
 191
 192/-- **The 3D polarized birth field satisfies the forced minimal-distinction property.** Same argument
 193as 2D via the octahedron `level_diff`: every 6-neighbour adjacency keeps the charge or flips it by
 194exactly one rung. So `UnitStep (polarized t) (E t)`. -/
 195theorem polarized_unitStep (t : ℕ) : UnitStep (polarized t) (E t) := by
 196  intro p hp
 197  rw [E, Finset.mem_filter] at hp
 198  by_cases h : polarized t p.1 = polarized t p.2
 199  · exact Or.inl (sub_eq_zero.mpr h)
 200  · rcases PolarizedBirthInterfaceCost.Octahedron.level_diff t p.1 p.2 hp.2 h with h1 | hm1
 201    · exact Or.inr (Or.inl h1)
 202    · exact Or.inr (Or.inr hm1)
 203
 204/-- The general graded-rung `totalCost` at `k = polarized t` is definitionally the Phase-55
 205`PolarizedBirthInterfaceCost.Octahedron.totalCost t` (3D). -/
 206theorem polarized_totalCost (t : ℕ) :
 207    totalCost (polarized t) (E t) = PolarizedBirthInterfaceCost.Octahedron.totalCost t := rfl
 208
 209/-- **The general law recovers the Phase-55 3D closed form.** Instantiating the graded-rung ledger at
 210the polarized octahedron field gives `totalCost = (8t^2 - 8t + 4) * J(phi)` (`t >= 1`): the dimension
 211`T8` forces (D=3) version of the binary special case of the graded-rung cost law. -/
 212theorem polarized_totalCost_card (t : ℕ) (ht : 1 ≤ t) :
 213    totalCost (polarized t) (E t) = (8 * t ^ 2 - 8 * t + 4) • Cost.Jcost Constants.phi := by
 214  rw [polarized_totalCost, PolarizedBirthInterfaceCost.Octahedron.totalCost_card t ht]
 215
 216end Octahedron
 217
 218end GradedRungCost
 219end Cosmology
 220end IndisputableMonolith
 221