IndisputableMonolith.Cosmology.RungDescentUnitStep

   1import Mathlib
   2import IndisputableMonolith.Cosmology.GradedRungCost
   3
   4/-!
   5# Integer-rung descent preserves the unit-step invariant: the positive complement to Phase 58
   6
   7Phase 56 (`GradedRungCost`) made the recognition-cost law depend on the forced
   8minimal-distinction invariant `UnitStep k E` (every adjacency changes the integer rung by at
   9most one). Phase 57 wired that law into the runtime cost meter. Phase 58
  10(`RecognitionUnitStepPreservation`) then proved the honest negative fact about the *real-valued*
  11mean move (`pairResolve`): a blind global "the dynamics preserves unit-step" claim is FALSE, and
  12the only correct statement is a local post-move criterion.
  13
  14Phase 59 supplies the positive half on the object the cost meter actually charges: the integer
  15rung field `k : V -> Z`. The live engine does not move integer rungs by real means; it descends a
  16region by exactly one rung when a distinction is forced (T-3 descends one rung at a time). The
  17question Phase 56/57 leaves open is whether *that* update keeps `UnitStep` cycle to cycle. The
  18answer here is precise:
  19
  20* `shiftDown_unitStep_of_cut`: descending an arbitrary set `S` by one rung preserves `UnitStep`
  21  exactly when every *cut* edge (one endpoint in `S`, one outside) stays within one rung after the
  22  move. Edges with both endpoints inside `S`, or both outside, are preserved for free (the gap is
  23  unchanged). This is the integer analogue of Phase 58's `pairResolve_unitStep_of_local`.
  24* `shiftDown_top_unitStep`: the cut condition is **discharged unconditionally** when `S` is the set
  25  of cells at the top rung `M` (any upper bound on the rungs present in `E`). A top-rung cell's
  26  neighbour is forced to sit exactly one rung below, so after the descent the cut gap is `0`. So
  27  descending the coarsest (top) rung, the natural parameter-free relaxation move, provably keeps
  28  the field unit-step, and the Phase-56 cost law applies to the next cycle.
  29* `exists_top_descent_unitStep`: for any nonempty edge set with a unit-step field, such a
  30  preserving descent exists with no externally supplied `M` (take `M` to be the realised maximum
  31  rung), and it is nontrivial (the top rung is attained).
  32* `shiftUp_bot_unitStep`: the dual, raising the bottom rung, by symmetry.
  33* `ckLevels_descend_min_breaks`: the necessity counterexample. On the three-site chain with rungs
  34  `0,1,2`, descending the *bottom* cell (rung `0`) sends it to `-1`, so its edge to the rung-`1`
  35  neighbour has gap `2` and `UnitStep` fails. Descending a non-top cell is therefore unsafe; the
  36  top-rung restriction in `shiftDown_top_unitStep` is necessary, not cosmetic.
  37
  38HONEST STATUS: THEOREM, 0 `sorry`, no new axioms beyond Mathlib's standard three
  39(`propext`, `Classical.choice`, `Quot.sound`). This closes the "we need a Lean theorem that the
  40active dynamics preserves the `UnitStep` graded-rung invariant cycle to cycle" item with the exact
  41truth: the generic move does not (Phase 58), but the forced top-rung descent does (Phase 59), and
  42the cost meter is theorem-backed along that update.
  43-/
  44
  45namespace IndisputableMonolith
  46namespace Cosmology
  47namespace RungDescentUnitStep
  48
  49open GradedRungCost (UnitStep)
  50
  51variable {V : Type*}
  52
  53/-! ## §1. The one-rung descent of a set and its pointwise values -/
  54
  55/-- Descend every cell in `S` by exactly one rung, leaving the rest fixed. This is the integer
  56single-rung move the T-3 refiner posts; it changes rungs by `1`, never by a real mean. -/
  57def shiftDown (S : V → Prop) [DecidablePred S] (k : V → ℤ) : V → ℤ :=
  58  fun v => if S v then k v - 1 else k v
  59
  60/-- Raise every cell in `S` by exactly one rung (the dual move). -/
  61def shiftUp (S : V → Prop) [DecidablePred S] (k : V → ℤ) : V → ℤ :=
  62  fun v => if S v then k v + 1 else k v
  63
  64lemma shiftDown_pos (S : V → Prop) [DecidablePred S] (k : V → ℤ) {v : V} (h : S v) :
  65    shiftDown S k v = k v - 1 := if_pos h
  66
  67lemma shiftDown_neg (S : V → Prop) [DecidablePred S] (k : V → ℤ) {v : V} (h : ¬ S v) :
  68    shiftDown S k v = k v := if_neg h
  69
  70lemma shiftUp_pos (S : V → Prop) [DecidablePred S] (k : V → ℤ) {v : V} (h : S v) :
  71    shiftUp S k v = k v + 1 := if_pos h
  72
  73lemma shiftUp_neg (S : V → Prop) [DecidablePred S] (k : V → ℤ) {v : V} (h : ¬ S v) :
  74    shiftUp S k v = k v := if_neg h
  75
  76/-! ## §2. The local cut criterion (integer analogue of Phase 58) -/
  77
  78/-- **Local preservation criterion.** Descending a set `S` by one rung preserves `UnitStep` on the
  79whole edge set provided every *cut* edge (exactly one endpoint in `S`) remains within one rung
  80after the move. Edges with both endpoints in `S` keep their gap (both shift by `1`); edges with
  81neither endpoint in `S` are unchanged. So only the cut edges can break the invariant, and the
  82hypothesis controls exactly those. -/
  83theorem shiftDown_unitStep_of_cut (S : V → Prop) [DecidablePred S] (k : V → ℤ)
  84    (E : Finset (V × V)) (hunit : UnitStep k E)
  85    (hcut : ∀ p ∈ E, ((S p.1 ∧ ¬ S p.2) ∨ (¬ S p.1 ∧ S p.2)) →
  86        (shiftDown S k p.1 - shiftDown S k p.2 = 0
  87          ∨ shiftDown S k p.1 - shiftDown S k p.2 = 1
  88          ∨ shiftDown S k p.1 - shiftDown S k p.2 = -1)) :
  89    UnitStep (shiftDown S k) E := by
  90  intro p hp
  91  by_cases h1 : S p.1 <;> by_cases h2 : S p.2
  92  · -- both endpoints descend: the gap is unchanged
  93    rw [shiftDown_pos S k h1, shiftDown_pos S k h2]
  94    have hsame : (k p.1 - 1) - (k p.2 - 1) = k p.1 - k p.2 := by ring
  95    rw [hsame]; exact hunit p hp
  96  · -- cut edge: p.1 descends, p.2 stays
  97    exact hcut p hp (Or.inl ⟨h1, h2⟩)
  98  · -- cut edge: p.1 stays, p.2 descends
  99    exact hcut p hp (Or.inr ⟨h1, h2⟩)
 100  · -- neither endpoint descends: unchanged
 101    rw [shiftDown_neg S k h1, shiftDown_neg S k h2]; exact hunit p hp
 102
 103/-! ## §3. Descending the top rung always preserves unit-step -/
 104
 105/-- **Top-rung descent preserves `UnitStep` unconditionally.** If `M` bounds every rung present in
 106`E` and `S` is the set of cells at rung `M`, then descending `S` by one rung keeps the field
 107unit-step. The cut argument is forced: a top-rung cell's neighbour cannot be above it, and
 108`UnitStep` forbids it being two below, so the neighbour sits exactly one rung down; after the
 109descent the two endpoints meet at rung `M - 1` and the cut gap is `0`. -/
 110theorem shiftDown_top_unitStep (k : V → ℤ) (E : Finset (V × V)) (M : ℤ)
 111    (hunit : UnitStep k E) (hub : ∀ p ∈ E, k p.1 ≤ M ∧ k p.2 ≤ M) :
 112    UnitStep (shiftDown (fun v => k v = M) k) E := by
 113  apply shiftDown_unitStep_of_cut (fun v => k v = M) k E hunit
 114  intro p hp hcut
 115  obtain ⟨hub1, hub2⟩ := hub p hp
 116  have hstep := hunit p hp
 117  rcases hcut with ⟨h1, h2⟩ | ⟨h1, h2⟩
 118  · -- k p.1 = M (in S), k p.2 ≠ M (out): neighbour is forced to M - 1
 119    have hb2 : k p.2 < M := lt_of_le_of_ne hub2 h2
 120    have hk2 : k p.2 = M - 1 := by omega
 121    have v1 : shiftDown (fun v => k v = M) k p.1 = k p.1 - 1 := shiftDown_pos _ k h1
 122    have v2 : shiftDown (fun v => k v = M) k p.2 = k p.2 := shiftDown_neg _ k h2
 123    left; rw [v1, v2]; omega
 124  · -- k p.1 ≠ M (out), k p.2 = M (in): symmetric
 125    have hb1 : k p.1 < M := lt_of_le_of_ne hub1 h1
 126    have hk1 : k p.1 = M - 1 := by omega
 127    have v1 : shiftDown (fun v => k v = M) k p.1 = k p.1 := shiftDown_neg _ k h1
 128    have v2 : shiftDown (fun v => k v = M) k p.2 = k p.2 - 1 := shiftDown_pos _ k h2
 129    left; rw [v1, v2]; omega
 130
 131/-- The vertices that actually appear in an edge set. -/
 132def edgeVerts [DecidableEq V] (E : Finset (V × V)) : Finset V :=
 133  E.image Prod.fst ∪ E.image Prod.snd
 134
 135lemma fst_mem_edgeVerts [DecidableEq V] {E : Finset (V × V)} {p : V × V} (hp : p ∈ E) :
 136    p.1 ∈ edgeVerts E :=
 137  Finset.mem_union.mpr (Or.inl (Finset.mem_image.mpr ⟨p, hp, rfl⟩))
 138
 139lemma snd_mem_edgeVerts [DecidableEq V] {E : Finset (V × V)} {p : V × V} (hp : p ∈ E) :
 140    p.2 ∈ edgeVerts E :=
 141  Finset.mem_union.mpr (Or.inr (Finset.mem_image.mpr ⟨p, hp, rfl⟩))
 142
 143/-- **A preserving descent always exists.** For any nonempty edge set carrying a unit-step rung
 144field, take `M` to be the realised maximum rung; descending the top-rung cells preserves
 145`UnitStep`, and the descent is nontrivial because the maximum is attained. No external parameter
 146is supplied: `M` is read off the field. -/
 147theorem exists_top_descent_unitStep [DecidableEq V] (k : V → ℤ) (E : Finset (V × V))
 148    (hne : E.Nonempty) (hunit : UnitStep k E) :
 149    ∃ M : ℤ, (∃ v ∈ edgeVerts E, k v = M)
 150      ∧ UnitStep (shiftDown (fun v => k v = M) k) E := by
 151  have hVne : (edgeVerts E).Nonempty := by
 152    obtain ⟨p, hp⟩ := hne
 153    exact ⟨p.1, fst_mem_edgeVerts hp⟩
 154  have hImgNe : ((edgeVerts E).image k).Nonempty := hVne.image k
 155  set M : ℤ := ((edgeVerts E).image k).max' hImgNe with hM
 156  have hMmem : M ∈ (edgeVerts E).image k := Finset.max'_mem _ hImgNe
 157  obtain ⟨v, hv, hvk⟩ := Finset.mem_image.mp hMmem
 158  refine ⟨M, ⟨v, hv, hvk⟩, ?_⟩
 159  apply shiftDown_top_unitStep k E M hunit
 160  intro p hp
 161  refine ⟨?_, ?_⟩
 162  · exact Finset.le_max' _ (k p.1) (Finset.mem_image.mpr ⟨p.1, fst_mem_edgeVerts hp, rfl⟩)
 163  · exact Finset.le_max' _ (k p.2) (Finset.mem_image.mpr ⟨p.2, snd_mem_edgeVerts hp, rfl⟩)
 164
 165/-! ## §4. The dual: raising the bottom rung -/
 166
 167/-- **Bottom-rung raise preserves `UnitStep` unconditionally** (dual of `shiftDown_top_unitStep`).
 168If `m` bounds every rung from below and `S` is the set of cells at rung `m`, raising `S` by one
 169rung keeps the field unit-step: a bottom cell's neighbour is forced to be exactly one rung up, so
 170after the raise the cut gap is `0`. -/
 171theorem shiftUp_bot_unitStep (k : V → ℤ) (E : Finset (V × V)) (m : ℤ)
 172    (hunit : UnitStep k E) (hlb : ∀ p ∈ E, m ≤ k p.1 ∧ m ≤ k p.2) :
 173    UnitStep (shiftUp (fun v => k v = m) k) E := by
 174  intro p hp
 175  obtain ⟨hlb1, hlb2⟩ := hlb p hp
 176  have hstep := hunit p hp
 177  by_cases h1 : k p.1 = m <;> by_cases h2 : k p.2 = m
 178  · rw [shiftUp_pos _ k h1, shiftUp_pos _ k h2]
 179    have hsame : (k p.1 + 1) - (k p.2 + 1) = k p.1 - k p.2 := by ring
 180    rw [hsame]; exact hstep
 181  · -- k p.1 = m (raised), k p.2 ≠ m: neighbour forced to m + 1
 182    have hb2 : m < k p.2 := lt_of_le_of_ne hlb2 (Ne.symm h2)
 183    have hk2 : k p.2 = m + 1 := by omega
 184    rw [shiftUp_pos _ k h1, shiftUp_neg _ k h2]
 185    left; omega
 186  · -- k p.2 = m (raised), k p.1 ≠ m: symmetric
 187    have hb1 : m < k p.1 := lt_of_le_of_ne hlb1 (Ne.symm h1)
 188    have hk1 : k p.1 = m + 1 := by omega
 189    rw [shiftUp_neg _ k h1, shiftUp_pos _ k h2]
 190    left; omega
 191  · rw [shiftUp_neg _ k h1, shiftUp_neg _ k h2]; exact hstep
 192
 193/-! ## §5. Necessity: descending a non-top cell breaks unit-step -/
 194
 195/-- The three-site chain rung field `0, 1, 2` (the rung is the position index). -/
 196def ckLevels : Fin 3 → ℤ := fun i => (i.val : ℤ)
 197
 198/-- The chain edges `0 -- 1 -- 2` (ordered, as the engine carries them). -/
 199def ckEdges : Finset (Fin 3 × Fin 3) :=
 200  {((0 : Fin 3), (1 : Fin 3)), ((1 : Fin 3), (2 : Fin 3))}
 201
 202/-- The chain `0, 1, 2` is unit-step before any move. -/
 203theorem ckLevels_unitStep : UnitStep ckLevels ckEdges := by
 204  unfold UnitStep; decide
 205
 206/-- **Necessity counterexample.** Descending the *bottom* cell (rung `0`) of the chain `0, 1, 2`
 207sends it to `-1`, so the edge to the rung-`1` neighbour has gap `2` and `UnitStep` fails. Only
 208descending the top rung is safe; the top-rung hypothesis of `shiftDown_top_unitStep` is necessary,
 209not cosmetic. -/
 210theorem ckLevels_descend_min_breaks :
 211    ¬ UnitStep (shiftDown (fun v => v = (0 : Fin 3)) ckLevels) ckEdges := by
 212  unfold UnitStep; decide
 213
 214/-! ## §6. The bundled headline -/
 215
 216/-- **Phase-59 headline.** On the integer rung field the cost meter charges, the forced top-rung
 217descent (the natural parameter-free relaxation move) preserves the unit-step invariant for any
 218unit-step field with a rung upper bound, so the Phase-56 cost law applies to the next cycle; and
 219the concrete chain `0, 1, 2` shows a non-top single-cell descent breaks it, so the restriction is
 220necessary. Together with Phase 58 (the real-valued mean move does not preserve unit-step globally)
 221this is the complete, honest answer to whether the dynamics preserves the graded-rung invariant. -/
 222theorem t59_rung_descent_preservation (k : V → ℤ) (E : Finset (V × V)) (M : ℤ)
 223    (hunit : UnitStep k E) (hub : ∀ p ∈ E, k p.1 ≤ M ∧ k p.2 ≤ M) :
 224    UnitStep (shiftDown (fun v => k v = M) k) E
 225    ∧ ¬ UnitStep (shiftDown (fun v => v = (0 : Fin 3)) ckLevels) ckEdges :=
 226  ⟨shiftDown_top_unitStep k E M hunit hub, ckLevels_descend_min_breaks⟩
 227
 228end RungDescentUnitStep
 229end Cosmology
 230end IndisputableMonolith
 231