IndisputableMonolith.Cosmology.RecognitionUnitStepPreservation

   1import Mathlib
   2import IndisputableMonolith.Cosmology.GradedRungCost
   3import IndisputableMonolith.Cosmology.RecognitionEquilibrium
   4
   5/-!
   6# Unit-step preservation for active recognition dynamics
   7
   8Phase 56 proved the graded-rung cost law under the forced minimal-distinction invariant
   9`UnitStep`: adjacent rungs differ by at most one. Phase 57 wired that law into the runtime
  10cost meter. The tempting next claim would be that the active mean-move dynamics
  11(`RecognitionEquilibrium.pairResolve`) preserves this invariant automatically.
  12
  13That claim is false.
  14
  15This module records the honest theorem layer:
  16
  17* `pairResolve_unitStep_of_local`: resolving a pair preserves the real-valued unit-step
  18  invariant provided every edge touching one of the two resolved endpoints remains
  19  within one rung after the move. Edges disjoint from the resolved pair are preserved
  20  for free by `pairResolve_other`.
  21* `chain3_pairResolve_breaks_unitStep`: a three-site chain with levels `0,1,2` is
  22  unit-step before the move, but resolving the first edge sends levels to
  23  `1/2,1/2,2`, so the second edge has gap `3/2` and the invariant fails.
  24
  25The upshot is precise: the live engine may use the Phase-56 cost law only after auditing
  26or proving the local unit-step condition for the update being applied. A blind global
  27"mean-move preserves UnitStep" lemma would be false.
  28
  29HONEST STATUS: THEOREM, 0 `sorry`, no new axioms beyond Mathlib's standard classical
  30ones. The counterexample is a theorem, not a numerical observation.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Cosmology
  35namespace RecognitionUnitStepPreservation
  36
  37open RecognitionEquilibrium
  38
  39/-! ## §1. Real-valued unit-step fields on a finite edge list -/
  40
  41/-- A real-valued version of the Phase-56 unit-step invariant: every listed edge has
  42level gap at most one. This is the right formulation for `pairResolve`, whose mean move
  43can create half-rungs even when the input levels are integer rungs. -/
  44def UnitStepReal {n : ℕ} (x : Fin n → ℝ) (E : List (Fin n × Fin n)) : Prop :=
  45  ∀ e ∈ E, |x e.1 - x e.2| ≤ 1
  46
  47/-- An edge touches the pair being resolved if either endpoint is one of the two
  48resolved vertices. -/
  49def EdgeTouches {n : ℕ} (i j : Fin n) (e : Fin n × Fin n) : Prop :=
  50  e.1 = i ∨ e.1 = j ∨ e.2 = i ∨ e.2 = j
  51
  52/-- **Local preservation criterion.** A `pairResolve` move preserves the unit-step
  53invariant on the whole edge list if every edge touching the resolved pair remains
  54unit-step after the move. Disjoint edges are unchanged by `pairResolve_other`, so the
  55old unit-step invariant carries them automatically.
  56
  57This is the exact condition the runtime must audit, or a later theorem must prove, before
  58applying the Phase-56 cost law to an actively updated field. -/
  59theorem pairResolve_unitStep_of_local {n : ℕ} (x : Fin n → ℝ) (E : List (Fin n × Fin n))
  60    (i j : Fin n) (hunit : UnitStepReal x E)
  61    (hlocal : ∀ e ∈ E, EdgeTouches i j e →
  62      |pairResolve x i j e.1 - pairResolve x i j e.2| ≤ 1) :
  63    UnitStepReal (pairResolve x i j) E := by
  64  intro e he
  65  by_cases ht : EdgeTouches i j e
  66  · exact hlocal e he ht
  67  · have h1i : e.1 ≠ i := by
  68      intro h; exact ht (Or.inl h)
  69    have h1j : e.1 ≠ j := by
  70      intro h; exact ht (Or.inr (Or.inl h))
  71    have h2i : e.2 ≠ i := by
  72      intro h; exact ht (Or.inr (Or.inr (Or.inl h)))
  73    have h2j : e.2 ≠ j := by
  74      intro h; exact ht (Or.inr (Or.inr (Or.inr h)))
  75    rw [pairResolve_other x h1i h1j, pairResolve_other x h2i h2j]
  76    exact hunit e he
  77
  78/-! ## §2. The global preservation claim is false -/
  79
  80def f0 : Fin 3 := ⟨0, by decide⟩
  81def f1 : Fin 3 := ⟨1, by decide⟩
  82def f2 : Fin 3 := ⟨2, by decide⟩
  83
  84/-- The three-site chain `0 -- 1 -- 2`. -/
  85def chain3Edges : List (Fin 3 × Fin 3) := [(f0, f1), (f1, f2)]
  86
  87/-- The initial levels `0, 1, 2`, written by cases over `Fin 3`. -/
  88def chain3Levels : Fin 3 → ℝ
  89  | ⟨0, _⟩ => 0
  90  | ⟨1, _⟩ => 1
  91  | ⟨2, _⟩ => 2
  92
  93@[simp] lemma chain3Levels_f0 : chain3Levels f0 = 0 := rfl
  94@[simp] lemma chain3Levels_f1 : chain3Levels f1 = 1 := rfl
  95@[simp] lemma chain3Levels_f2 : chain3Levels f2 = 2 := rfl
  96
  97/-- The chain `0,1,2` is unit-step before any resolution. -/
  98theorem chain3_unitStep : UnitStepReal chain3Levels chain3Edges := by
  99  intro e he
 100  simp [chain3Edges] at he
 101  rcases he with rfl | he
 102  · norm_num
 103  · rcases he with rfl
 104    norm_num
 105
 106/-- After resolving the first edge `(0,1)`, the second edge `(1,2)` has gap `3/2`. -/
 107lemma chain3_resolved_second_gap :
 108    |pairResolve chain3Levels f0 f1 f1 - pairResolve chain3Levels f0 f1 f2| = (3 / 2 : ℝ) := by
 109  have hf2_ne_f0 : f2 ≠ f0 := by decide
 110  have hf2_ne_f1 : f2 ≠ f1 := by decide
 111  rw [pairResolve_at_j, pairResolve_other chain3Levels hf2_ne_f0 hf2_ne_f1]
 112  norm_num
 113
 114/-- **Counterexample.** A unit-step field need not remain unit-step after a mean-move
 115resolution. The three-site chain `0 -- 1 -- 2` starts with gaps `1` and `1`; resolving
 116the first edge gives levels `1/2, 1/2, 2`, so the second edge has gap `3/2 > 1`.
 117
 118This blocks the false global theorem "mean-move preserves UnitStep". The correct theorem
 119is the local criterion `pairResolve_unitStep_of_local` above. -/
 120theorem chain3_pairResolve_breaks_unitStep :
 121    ¬ UnitStepReal (pairResolve chain3Levels f0 f1) chain3Edges := by
 122  intro h
 123  have hedge : (f1, f2) ∈ chain3Edges := by
 124    simp [chain3Edges]
 125  have hstep := h (f1, f2) hedge
 126  rw [chain3_resolved_second_gap] at hstep
 127  norm_num at hstep
 128
 129/-- Phase-58 headline: active mean-move dynamics does not preserve unit-step globally;
 130it preserves it exactly under the local post-move edge condition, and the 3-chain
 131counterexample shows that condition is necessary rather than cosmetic. -/
 132theorem t58_unitStep_preservation_honest :
 133    (∀ {n : ℕ} (x : Fin n → ℝ) (E : List (Fin n × Fin n)) (i j : Fin n),
 134        UnitStepReal x E →
 135        (∀ e ∈ E, EdgeTouches i j e →
 136          |pairResolve x i j e.1 - pairResolve x i j e.2| ≤ 1) →
 137        UnitStepReal (pairResolve x i j) E)
 138    ∧ ¬ UnitStepReal (pairResolve chain3Levels f0 f1) chain3Edges :=
 139  ⟨fun {n} x E i j hunit hlocal =>
 140    pairResolve_unitStep_of_local (n := n) x E i j hunit hlocal,
 141   chain3_pairResolve_breaks_unitStep⟩
 142
 143end RecognitionUnitStepPreservation
 144end Cosmology
 145end IndisputableMonolith
 146