IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2LatticeKindRule
   2import IndisputableMonolith.LedgerPostingAdjacency
   3
   4/-!
   5# Gap 2, fifth arc: does the posting dynamics force the counts-only premise?
   6
   7The chain of named premises behind Gap 2's measure, as the last three arcs left it: the weight
   8is size-blind if the cost is kind-only (`Gap2PostingCostDerivation`); the cost is kind-only if
   9its charge is counts-only (`Gap2KindRule`, the named premise `ChargesCountsOnly`); the charge
  10is counts-only if the lattice imbalance and magnitude are (`Gap2LatticeKindRule`, the named
  11premise `LatticeChargesCountsOnly`).  None of those is forced at its own layer, and the fourth
  12arc flagged the successor as the ledger *dynamics*: the posting rules that produce the states,
  13not the state type.  This module settles the dynamics, and the answer is the sharpest of the
  14three.
  15
  16**The committed answer is no, and for a stronger reason than at the upper layers: the dynamics
  17excludes nothing.**  A posting step increments one account's debit or credit column by one
  18quantum (`LedgerPostingAdjacency.post`, `PostingStep`), and a run is a schedule of such steps.
  19From the balanced zero ledger, *every* ledger with nonnegative columns is reachable
  20(`postReachable_zero_of_nonneg`: forward reachability; posts only ever raise a column, so
  21ledgers with a negative column are not reachable and the statement is not ergodicity), so
  22*every* integer imbalance configuration is the `phi` of a reachable ledger
  23(`imbalance_realized`), and is reached by an explicit posting schedule
  24(`imbalance_realized_by_schedule`).  A dynamics that reaches every nonnegative state excludes
  25no imbalance; in particular it reaches the incidence-reading and index-reading imbalances, the
  26two families the earlier arcs exhibited non-counts-only members of (the incidence reading on
  27complexes mixing at least one proper edge with at least one loop, the index reading).
  28
  29The two conjuncts of the fourth arc's dual premise each fall, for their own reasons:
  30
  31* **Imbalance.**  The dynamics produces every `phi`, so it produces the countermodel's.  Stated
  32  at the schedule level, where the premise would have to live: there is an explicitly exhibited
  33  posting schedule on the two-bridge witness whose imbalance after one tick is not kind-constant
  34  (`schedule_countermodel_not_countsOnly`), so counts-only is not a theorem about schedules.
  35
  36* **Magnitude.**  This conjunct falls not to reachability but to silence: the posting step acts
  37  on the debit and credit columns of a `Recognition.Ledger`, which has no magnitude field, so
  38  posting says nothing about magnitude at all.  The `DualEntryStrainState` enrichment adds `mag`
  39  separately, and `DualEntryStrainState.ofLedger` attaches *any* nonnegative magnitude function
  40  to *any* reachable ledger with unit flux, so every lattice state the fourth arc admitted is
  41  dynamically generable from balance (`dynamics_produces_incidence_countermodel`).  Whether the
  42  produced incidence state is itself a countermodel depends on the edge-kind mix: the incidence
  43  imbalance is `1` on proper edge letters and `0` elsewhere, so it is kind-constant, hence
  44  counts-only, exactly when the complex's edges are all proper or all loops (`twoBridges` and
  45  `twoLoops` alike), and it fails counts-only exactly when the complex carries at least one
  46  proper edge and at least one loop.  The §4 schedule countermodel on `twoBridges` is a
  47  different witness of a different kind: its imbalance after one tick is `1` on edge letter 0
  48  and `0` on edge letter 1, which is not the incidence imbalance of any complex.
  49
  50**The recursion bottoms out at the three layers examined.**  The letter-cost space does not
  51force counts-only (third arc), the lattice state type does not (fourth arc), and the posting
  52dynamics does not (this arc); the kernel content is `ledger_forces_countsOnly_at_no_layer`,
  53the conjunction of those three negative receipts.  Whether some deeper layer than the posting
  54step could force it is a meta-question the theorems do not address, because the library carries
  55no layer below the posting step.  What counts-only can still be is a law about the *actual*
  56schedule nature executes: which account posts, which side, at each tick.  That is a physical
  57premise about one run, not a theorem about the space of runs, and it is named
  58`CountsOnlySchedule` in §4.  Whether the universe's schedule satisfies it is the open question
  59this arc hands to the measure track; it cannot be settled by inspecting the ledger, because
  60the ledger admits every schedule.
  61
  62## What this settles for the measure track
  63
  64Track A of `QG/plans/QG_Full_Theory_Completion_20260729.html` asked (step A1.1): does the
  65posting dynamics force `LatticeChargesCountsOnly`?  Answer: no, with receipts, and the premise
  66is now named at the dynamics layer per the plan's hard stop.  Consequence for the next step:
  67the measure derivation cannot come from any restriction on the charge picture, because no
  68charge restriction is available at any layer of the ledger.  The remaining route is the
  69counting structure itself (the canonical pinning and the orbit count), which is Track A1.2's
  70target.
  71-/
  72
  73namespace IndisputableMonolith
  74namespace Gravity
  75namespace SevenGaps
  76namespace Gap2DynamicsKindRule
  77
  78open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
  79open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation Gap2KindRule
  80open Gap2LatticeKindRule
  81open Analysis.RecognitionDualEntryEnrichment4D
  82
  83noncomputable section
  84
  85variable {Λ : Type} [Fintype Λ] [DecidableEq Λ]
  86
  87/-! ## §1. Posting on a generic discrete carrier, and total reachability -/
  88
  89/-- The balanced zero ledger: every column empty.  This is the state the counted histories are
  90pinned to by `CanonicalHistory.state_canonical`, seen now as the *initial condition* of the
  91posting dynamics rather than as a selection among states. -/
  92def zeroLedger : Recognition.Ledger (discreteCarrier Λ) where
  93  debit := fun _ => 0
  94  credit := fun _ => 0
  95
  96/-- One posting step on the generic carrier: increment one account's debit or credit column by
  97one quantum.  This is `LedgerPostingAdjacency.post` lifted from `Fin d` to an arbitrary
  98decidable finite carrier; the step relation it generates is the whole of the dynamics. -/
  99def postAt (L : Recognition.Ledger (discreteCarrier Λ)) (k : Λ)
 100    (s : LedgerPostingAdjacency.Side) : Recognition.Ledger (discreteCarrier Λ) :=
 101  match s with
 102  | .debit => { debit := fun i => if i = k then L.debit i + 1 else L.debit i
 103                credit := L.credit }
 104  | .credit => { debit := L.debit
 105                 credit := fun i => if i = k then L.credit i + 1 else L.credit i }
 106
 107/-- **Reachability.**  Ledger `L₂` is reachable from `L₁` by a finite sequence of posting
 108steps.  Defined as a closure so the reachability statements below are about the step relation
 109itself, not about any particular scheduling device. -/
 110inductive PostReachable : Recognition.Ledger (discreteCarrier Λ) →
 111    Recognition.Ledger (discreteCarrier Λ) → Prop where
 112  | refl (L : Recognition.Ledger (discreteCarrier Λ)) : PostReachable L L
 113  | step {L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)} (k : Λ)
 114      (s : LedgerPostingAdjacency.Side) :
 115      PostReachable L₁ L₂ → PostReachable L₁ (postAt L₂ k s)
 116
 117@[simp] theorem phi_zeroLedger (i : Λ) : Recognition.phi zeroLedger i = 0 := rfl
 118
 119theorem phi_postAt_debit_self (L : Recognition.Ledger (discreteCarrier Λ)) (k : Λ) :
 120    Recognition.phi (postAt L k .debit) k = Recognition.phi L k + 1 := by
 121  have h1 : (postAt L k .debit).debit k = L.debit k + 1 := if_pos rfl
 122  have h2 : (postAt L k .debit).credit k = L.credit k := rfl
 123  show (postAt L k .debit).debit k - (postAt L k .debit).credit k
 124      = L.debit k - L.credit k + 1
 125  rw [h1, h2]
 126  omega
 127
 128theorem phi_postAt_credit_self (L : Recognition.Ledger (discreteCarrier Λ)) (k : Λ) :
 129    Recognition.phi (postAt L k .credit) k = Recognition.phi L k - 1 := by
 130  have h1 : (postAt L k .credit).debit k = L.debit k := rfl
 131  have h2 : (postAt L k .credit).credit k = L.credit k + 1 := if_pos rfl
 132  show (postAt L k .credit).debit k - (postAt L k .credit).credit k
 133      = L.debit k - L.credit k - 1
 134  rw [h1, h2]
 135  omega
 136
 137theorem phi_postAt_ne (L : Recognition.Ledger (discreteCarrier Λ)) {i k : Λ} (h : i ≠ k)
 138    (s : LedgerPostingAdjacency.Side) :
 139    Recognition.phi (postAt L k s) i = Recognition.phi L i := by
 140  cases s with
 141  | debit =>
 142    have h1 : (postAt L k .debit).debit i = L.debit i := if_neg h
 143    have h2 : (postAt L k .debit).credit i = L.credit i := rfl
 144    show (postAt L k .debit).debit i - (postAt L k .debit).credit i
 145        = L.debit i - L.credit i
 146    rw [h1, h2]
 147  | credit =>
 148    have h1 : (postAt L k .credit).debit i = L.debit i := rfl
 149    have h2 : (postAt L k .credit).credit i = L.credit i := if_neg h
 150    show (postAt L k .credit).debit i - (postAt L k .credit).credit i
 151        = L.debit i - L.credit i
 152    rw [h1, h2]
 153
 154/-- Ledger extensionality, pointwise. -/
 155theorem ledger_ext {L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)}
 156    (hd : ∀ i, L₁.debit i = L₂.debit i) (hc : ∀ i, L₁.credit i = L₂.credit i) :
 157    L₁ = L₂ := by
 158  obtain ⟨d₁, c₁⟩ := L₁
 159  obtain ⟨d₂, c₂⟩ := L₂
 160  simp only [IndisputableMonolith.Recognition.Ledger.mk.injEq]
 161  exact ⟨funext fun i => hd i, funext fun i => hc i⟩
 162
 163/-- The total column mass: sum of absolute column values.  From zero, each posting step raises
 164mass by exactly one, so mass is the induction measure for reachability. -/
 165def mass (L : Recognition.Ledger (discreteCarrier Λ)) : ℕ :=
 166  ∑ i : Λ, (Int.natAbs (L.debit i) + Int.natAbs (L.credit i))
 167
 168/-- A ledger of zero mass is the zero ledger. -/
 169theorem eq_zeroLedger_of_mass_zero {L : Recognition.Ledger (discreteCarrier Λ)}
 170    (hm : mass L = 0) : L = zeroLedger := by
 171  have hm' : (∑ i : Λ, (Int.natAbs (L.debit i) + Int.natAbs (L.credit i))) = 0 := hm
 172  have h0 : ∀ i : Λ, Int.natAbs (L.debit i) + Int.natAbs (L.credit i) = 0 := by
 173    have hs := (Finset.sum_eq_zero_iff_of_nonneg (fun i _ => Nat.zero_le _)).mp hm'
 174    exact fun i => hs i (Finset.mem_univ i)
 175  have hd : ∀ i, L.debit i = 0 := fun i => by have := h0 i; omega
 176  have hc : ∀ i, L.credit i = 0 := fun i => by have := h0 i; omega
 177  apply ledger_ext
 178  · intro i; show L.debit i = 0; exact hd i
 179  · intro i; show L.credit i = 0; exact hc i
 180
 181/-- A nonzero nonnegative ledger has a coordinate with a positive column. -/
 182theorem exists_pos_of_ne_zero {L : Recognition.Ledger (discreteCarrier Λ)}
 183    (hnn : ∀ i, 0 ≤ L.debit i ∧ 0 ≤ L.credit i) (hne : L ≠ zeroLedger) :
 184    ∃ i, 0 < L.debit i ∨ 0 < L.credit i := by
 185  by_contra h
 186  push_neg at h
 187  apply hne
 188  apply ledger_ext
 189  · intro i
 190    have hi := (h i).1
 191    have hj := (hnn i).1
 192    show L.debit i = 0
 193    omega
 194  · intro i
 195    have hi := (h i).2
 196    have hj := (hnn i).2
 197    show L.credit i = 0
 198    omega
 199
 200/-- The predecessor of a nonnegative ledger along a positive column: decrement that column at
 201one coordinate.  The ledger is then the post of its predecessor at that coordinate. -/
 202def predOf (L : Recognition.Ledger (discreteCarrier Λ)) (k : Λ)
 203    (s : LedgerPostingAdjacency.Side) : Recognition.Ledger (discreteCarrier Λ) :=
 204  match s with
 205  | .debit => { debit := fun i => if i = k then L.debit i - 1 else L.debit i
 206                credit := L.credit }
 207  | .credit => { debit := L.debit
 208                 credit := fun i => if i = k then L.credit i - 1 else L.credit i }
 209
 210theorem postAt_predOf (L : Recognition.Ledger (discreteCarrier Λ)) (k : Λ)
 211    (s : LedgerPostingAdjacency.Side)
 212    (hpos : match s with | .debit => 0 < L.debit k | .credit => 0 < L.credit k) :
 213    postAt (predOf L k s) k s = L := by
 214  cases s with
 215  | debit =>
 216    apply ledger_ext
 217    · intro i
 218      by_cases hik : i = k
 219      · subst i
 220        have h1 : (postAt (predOf L k .debit) k .debit).debit k
 221            = (predOf L k .debit).debit k + 1 := if_pos rfl
 222        have h2 : (predOf L k .debit).debit k = L.debit k - 1 := if_pos rfl
 223        have h3 : (postAt (predOf L k .debit) k .debit).credit k
 224            = (predOf L k .debit).credit k := rfl
 225        show (postAt (predOf L k .debit) k .debit).debit k = L.debit k
 226        rw [h1, h2]
 227        omega
 228      · have h1 : (postAt (predOf L k .debit) k .debit).debit i
 229            = (predOf L k .debit).debit i := if_neg hik
 230        have h2 : (predOf L k .debit).debit i = L.debit i := if_neg hik
 231        show (postAt (predOf L k .debit) k .debit).debit i = L.debit i
 232        rw [h1, h2]
 233    · intro i
 234      show (postAt (predOf L k .debit) k .debit).credit i = L.credit i
 235      rfl
 236  | credit =>
 237    apply ledger_ext
 238    · intro i
 239      show (postAt (predOf L k .credit) k .credit).debit i = L.debit i
 240      rfl
 241    · intro i
 242      by_cases hik : i = k
 243      · subst i
 244        have h1 : (postAt (predOf L k .credit) k .credit).credit k
 245            = (predOf L k .credit).credit k + 1 := if_pos rfl
 246        have h2 : (predOf L k .credit).credit k = L.credit k - 1 := if_pos rfl
 247        show (postAt (predOf L k .credit) k .credit).credit k = L.credit k
 248        rw [h1, h2]
 249        omega
 250      · have h1 : (postAt (predOf L k .credit) k .credit).credit i
 251            = (predOf L k .credit).credit i := if_neg hik
 252        have h2 : (predOf L k .credit).credit i = L.credit i := if_neg hik
 253        show (postAt (predOf L k .credit) k .credit).credit i = L.credit i
 254        rw [h1, h2]
 255
 256theorem predOf_nonneg {L : Recognition.Ledger (discreteCarrier Λ)}
 257    (hnn : ∀ i, 0 ≤ L.debit i ∧ 0 ≤ L.credit i) (k : Λ)
 258    (s : LedgerPostingAdjacency.Side)
 259    (hpos : match s with | .debit => 0 < L.debit k | .credit => 0 < L.credit k) :
 260    ∀ i, 0 ≤ (predOf L k s).debit i ∧ 0 ≤ (predOf L k s).credit i := by
 261  intro i
 262  cases s with
 263  | debit =>
 264    by_cases hik : i = k
 265    · subst i
 266      have hd : (predOf L k .debit).debit k = L.debit k - 1 := if_pos rfl
 267      have hc : (predOf L k .debit).credit k = L.credit k := rfl
 268      rw [hd, hc]
 269      have hk := hnn k
 270      omega
 271    · have hd : (predOf L k .debit).debit i = L.debit i := if_neg hik
 272      have hc : (predOf L k .debit).credit i = L.credit i := rfl
 273      rw [hd, hc]
 274      exact hnn i
 275  | credit =>
 276    by_cases hik : i = k
 277    · subst i
 278      have hd : (predOf L k .credit).debit k = L.debit k := rfl
 279      have hc : (predOf L k .credit).credit k = L.credit k - 1 := if_pos rfl
 280      rw [hd, hc]
 281      have hk := hnn k
 282      omega
 283    · have hd : (predOf L k .credit).debit i = L.debit i := rfl
 284      have hc : (predOf L k .credit).credit i = L.credit i := if_neg hik
 285      rw [hd, hc]
 286      exact hnn i
 287
 288/-- The predecessor has strictly smaller mass. -/
 289theorem mass_predOf_lt {L : Recognition.Ledger (discreteCarrier Λ)}
 290    (hnn : ∀ i, 0 ≤ L.debit i ∧ 0 ≤ L.credit i) (k : Λ)
 291    (s : LedgerPostingAdjacency.Side)
 292    (hpos : match s with | .debit => 0 < L.debit k | .credit => 0 < L.credit k) :
 293    mass (predOf L k s) < mass L := by
 294  cases s with
 295  | debit =>
 296    have hper : ∀ i ∈ Finset.univ.erase k,
 297        Int.natAbs ((predOf L k .debit).debit i) + Int.natAbs ((predOf L k .debit).credit i)
 298          = Int.natAbs (L.debit i) + Int.natAbs (L.credit i) := by
 299      intro i hi
 300      have hik : i ≠ k := Finset.ne_of_mem_erase hi
 301      have hd : (predOf L k .debit).debit i = L.debit i := if_neg hik
 302      have hc : (predOf L k .debit).credit i = L.credit i := rfl
 303      rw [hd, hc]
 304    have hsplit₁ : mass (predOf L k .debit)
 305        = (Int.natAbs ((predOf L k .debit).debit k) + Int.natAbs ((predOf L k .debit).credit k))
 306          + ∑ i ∈ Finset.univ.erase k,
 307            (Int.natAbs ((predOf L k .debit).debit i) + Int.natAbs ((predOf L k .debit).credit i)) := by
 308      show (∑ i : Λ, (Int.natAbs ((predOf L k .debit).debit i)
 309            + Int.natAbs ((predOf L k .debit).credit i))) = _
 310      exact (Finset.add_sum_erase _ _ (Finset.mem_univ k)).symm
 311    have hsplit₂ : mass L
 312        = (Int.natAbs (L.debit k) + Int.natAbs (L.credit k))
 313          + ∑ i ∈ Finset.univ.erase k, (Int.natAbs (L.debit i) + Int.natAbs (L.credit i)) := by
 314      show (∑ i : Λ, (Int.natAbs (L.debit i) + Int.natAbs (L.credit i))) = _
 315      exact (Finset.add_sum_erase _ _ (Finset.mem_univ k)).symm
 316    have hkk : (predOf L k .debit).debit k = L.debit k - 1 := if_pos rfl
 317    have hkc : (predOf L k .debit).credit k = L.credit k := rfl
 318    rw [hsplit₁, Finset.sum_congr rfl hper, hsplit₂, hkk, hkc]
 319    have hc : 0 < L.debit k := hpos
 320    have h1 : Int.natAbs (L.debit k - 1) = Int.natAbs (L.debit k) - 1 := by
 321      omega
 322    rw [h1]
 323    omega
 324  | credit =>
 325    have hper : ∀ i ∈ Finset.univ.erase k,
 326        Int.natAbs ((predOf L k .credit).debit i) + Int.natAbs ((predOf L k .credit).credit i)
 327          = Int.natAbs (L.debit i) + Int.natAbs (L.credit i) := by
 328      intro i hi
 329      have hik : i ≠ k := Finset.ne_of_mem_erase hi
 330      have hd : (predOf L k .credit).debit i = L.debit i := rfl
 331      have hc : (predOf L k .credit).credit i = L.credit i := if_neg hik
 332      rw [hd, hc]
 333    have hsplit₁ : mass (predOf L k .credit)
 334        = (Int.natAbs ((predOf L k .credit).debit k) + Int.natAbs ((predOf L k .credit).credit k))
 335          + ∑ i ∈ Finset.univ.erase k,
 336            (Int.natAbs ((predOf L k .credit).debit i) + Int.natAbs ((predOf L k .credit).credit i)) := by
 337      show (∑ i : Λ, (Int.natAbs ((predOf L k .credit).debit i)
 338            + Int.natAbs ((predOf L k .credit).credit i))) = _
 339      exact (Finset.add_sum_erase _ _ (Finset.mem_univ k)).symm
 340    have hsplit₂ : mass L
 341        = (Int.natAbs (L.debit k) + Int.natAbs (L.credit k))
 342          + ∑ i ∈ Finset.univ.erase k, (Int.natAbs (L.debit i) + Int.natAbs (L.credit i)) := by
 343      show (∑ i : Λ, (Int.natAbs (L.debit i) + Int.natAbs (L.credit i))) = _
 344      exact (Finset.add_sum_erase _ _ (Finset.mem_univ k)).symm
 345    have hkk : (predOf L k .credit).debit k = L.debit k := rfl
 346    have hkc : (predOf L k .credit).credit k = L.credit k - 1 := if_pos rfl
 347    rw [hsplit₁, Finset.sum_congr rfl hper, hsplit₂, hkk, hkc]
 348    have hc : 0 < L.credit k := hpos
 349    have h1 : Int.natAbs (L.credit k - 1) = Int.natAbs (L.credit k) - 1 := by
 350      omega
 351    rw [h1]
 352    omega
 353
 354/-- **THEOREM (the dynamics reaches every nonnegative ledger).**  From the balanced zero
 355ledger, every ledger with nonnegative columns is reachable by a finite sequence of posting
 356steps.  Proof: mass induction through the predecessor, which is legal because a nonzero
 357nonnegative ledger is the post of its predecessor.  Scope: this is forward reachability, not
 358ergodicity; a posting step only ever raises a column, so there is no return to lower-mass
 359states and no ledger with a negative column is reachable.  What the theorem supports is that
 360the dynamics excludes no nonnegative state, and therefore cannot force any restriction on the
 361imbalances of the states it produces. -/
 362theorem postReachable_zero_of_nonneg :
 363    ∀ N : ℕ, ∀ L : Recognition.Ledger (discreteCarrier Λ),
 364      mass L ≤ N → (∀ i, 0 ≤ L.debit i ∧ 0 ≤ L.credit i) →
 365      PostReachable zeroLedger L := by
 366  intro N
 367  induction N with
 368  | zero =>
 369    intro L hm _
 370    have hz : mass L = 0 := Nat.le_zero.mp hm
 371    rw [eq_zeroLedger_of_mass_zero hz]
 372    exact PostReachable.refl _
 373  | succ N IH =>
 374    intro L hm hnn
 375    by_cases hne : L = zeroLedger
 376    · subst hne
 377      exact PostReachable.refl _
 378    · obtain ⟨k, hk⟩ := exists_pos_of_ne_zero hnn hne
 379      cases hk with
 380      | inl hpos =>
 381        have hlt : mass (predOf L k .debit) < mass L := mass_predOf_lt hnn k .debit hpos
 382        rw [← postAt_predOf L k .debit hpos]
 383        exact PostReachable.step k .debit
 384          (IH (predOf L k .debit) (by omega) (predOf_nonneg hnn k .debit hpos))
 385      | inr hpos =>
 386        have hlt : mass (predOf L k .credit) < mass L := mass_predOf_lt hnn k .credit hpos
 387        rw [← postAt_predOf L k .credit hpos]
 388        exact PostReachable.step k .credit
 389          (IH (predOf L k .credit) (by omega) (predOf_nonneg hnn k .credit hpos))
 390
 391/-! ## §2. Every imbalance is realized from balance, by an explicit schedule -/
 392
 393/-- **THEOREM (every integer imbalance is the phi of a reachable ledger).**  Given any integer
 394configuration `φ`, the ledger with `debit = max φ 0`, `credit = max (-φ) 0` is nonnegative, has
 395`phi = φ`, and is reachable from balance by `postReachable_zero_of_nonneg`.  The dynamics
 396produces every imbalance pattern, the incidence-reading and index-reading ones included. -/
 397theorem imbalance_realized (φ : Λ → ℤ) :
 398    ∃ L : Recognition.Ledger (discreteCarrier Λ),
 399      (∀ i, 0 ≤ L.debit i ∧ 0 ≤ L.credit i) ∧
 400      PostReachable zeroLedger L ∧ Recognition.phi L = φ := by
 401  refine ⟨{ debit := fun i => max (φ i) 0, credit := fun i => max (-(φ i)) 0 }, ?_, ?_, ?_⟩
 402  · intro i
 403    exact ⟨le_max_right _ _, le_max_right _ _⟩
 404  · exact postReachable_zero_of_nonneg (mass _) _ (Nat.le_refl _)
 405      (fun i => ⟨le_max_right _ _, le_max_right _ _⟩)
 406  · funext i
 407    show max (φ i) 0 - max (-(φ i)) 0 = φ i
 408    by_cases h : 0 ≤ φ i
 409    · rw [max_eq_left h, max_eq_right (by omega : -(φ i) ≤ 0)]
 410      omega
 411    · rw [max_eq_right (by omega : φ i ≤ 0), max_eq_left (by omega : 0 ≤ -(φ i))]
 412      omega
 413
 414/-- A posting schedule on the carrier: at each tick, either an idle tick or a named account
 415posting on a named side.  This is the free variable of the dynamics, the one thing the ledger
 416structure does not constrain. -/
 417abbrev Schedule (Λ : Type) := ℕ → Option (Λ × LedgerPostingAdjacency.Side)
 418
 419/-- Run a schedule forward from an initial ledger; idle ticks leave the state unchanged. -/
 420def runSchedule (L₀ : Recognition.Ledger (discreteCarrier Λ)) (sched : Schedule Λ) :
 421    ℕ → Recognition.Ledger (discreteCarrier Λ)
 422  | 0 => L₀
 423  | (t + 1) => match sched t with
 424    | none => runSchedule L₀ sched t
 425    | some (k, s) => postAt (runSchedule L₀ sched t) k s
 426
 427/-- The imbalance after `t` ticks of a schedule from balance. -/
 428def phiAfter (sched : Schedule Λ) (t : ℕ) : Λ → ℤ :=
 429  Recognition.phi (runSchedule zeroLedger sched t)
 430
 431/-- Runs agree while their schedules agree: only ticks below `t` matter at tick `t`. -/
 432theorem runSchedule_eq_of_agree_below (L₀ : Recognition.Ledger (discreteCarrier Λ))
 433    {sched₁ sched₂ : Schedule Λ} {t : ℕ}
 434    (h : ∀ u, u < t → sched₁ u = sched₂ u) :
 435    runSchedule L₀ sched₁ t = runSchedule L₀ sched₂ t := by
 436  induction t with
 437  | zero => rfl
 438  | succ u IH =>
 439    have hu : sched₁ u = sched₂ u := h u (Nat.lt_succ_self u)
 440    have hpre : runSchedule L₀ sched₁ u = runSchedule L₀ sched₂ u :=
 441      IH (fun w hw => h w (Nat.lt_trans hw (Nat.lt_succ_self u)))
 442    simp only [runSchedule, hu, hpre]
 443
 444/-- Every run state is reachable: the run is one presentation of reachability. -/
 445theorem postReachable_run (sched : Schedule Λ) (t : ℕ) :
 446    PostReachable zeroLedger (runSchedule zeroLedger sched t) := by
 447  induction t with
 448  | zero => exact PostReachable.refl _
 449  | succ u IH =>
 450    simp only [runSchedule]
 451    cases hs : sched u with
 452    | none => exact IH
 453    | some instr =>
 454      obtain ⟨k, s⟩ := instr
 455      exact PostReachable.step k s IH
 456
 457/-- Every reachable state is reached by some schedule at some tick. -/
 458theorem exists_schedule_of_reachable {L : Recognition.Ledger (discreteCarrier Λ)}
 459    (h : PostReachable zeroLedger L) :
 460    ∃ (sched : Schedule Λ) (t : ℕ), runSchedule zeroLedger sched t = L := by
 461  induction h with
 462  | refl => exact ⟨fun _ => none, 0, rfl⟩
 463  | step k s _ IH =>
 464    obtain ⟨sched, t, ht⟩ := IH
 465    refine ⟨Function.update sched t (some (k, s)), t + 1, ?_⟩
 466    have hagree : ∀ u, u < t → Function.update sched t (some (k, s)) u = sched u :=
 467      fun u hu => Function.update_of_ne (Nat.ne_of_lt hu) _ _
 468    have hpre := runSchedule_eq_of_agree_below zeroLedger hagree
 469    simp only [runSchedule, Function.update_self, hpre, ht]
 470
 471/-- **THEOREM (every imbalance is realized by an explicit schedule).**  The schedule form of
 472`imbalance_realized`: there is a schedule and a tick at which the run's imbalance from balance
 473is exactly `φ`. -/
 474theorem imbalance_realized_by_schedule (φ : Λ → ℤ) :
 475    ∃ (sched : Schedule Λ) (t : ℕ), phiAfter sched t = φ := by
 476  obtain ⟨L, _, hreach, hphi⟩ := imbalance_realized φ
 477  obtain ⟨sched, t, ht⟩ := exists_schedule_of_reachable hreach
 478  exact ⟨sched, t, by
 479    show Recognition.phi (runSchedule zeroLedger sched t) = φ
 480    rw [ht]
 481    exact hphi⟩
 482
 483/-! ## §3. The dynamics produces the countermodel, on the actual posting alphabet -/
 484
 485/-- The incidence imbalance on a complex's posting alphabet: one quantum on every proper edge
 486letter, nothing elsewhere.  This is the `phi` of the fourth arc's countermodel
 487`incidencePhiLattice`, exhibited as a target configuration for the dynamics. -/
 488def incidenceImbalance {B : ℕ} (K : BoundedComplex B) : PostingAlphabet K → ℤ
 489  | Sum.inr (Sum.inl e) => if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then 1 else 0
 490  | _ => 0
 491
 492/-- **THEOREM (the dynamics produces the incidence-reading countermodel).**  On every complex's
 493posting alphabet there is a ledger, reachable from balance, whose imbalance is exactly the
 494incidence imbalance; and that ledger lifts, with any nonnegative magnitude function whatever,
 495to a `DualEntryStrainState` with that imbalance and that magnitude.  The countermodel state the
 496counts-only premise exists to exclude is not an edge case the dynamics fails to generate: the
 497dynamics generates it from balance, one posting at a time, and the magnitude factor rides
 498along for free because the posting step never touches it.  Scope, stated exactly: the
 499incidence imbalance is `1` on proper edge letters and `0` on every other letter, so the
 500produced state is counts-only exactly when the complex's edges are all proper or all loops,
 501and is a countermodel exactly when the complex carries at least one proper edge and at least
 502one loop.  The `∀ K` statement holds on every complex; "countermodel" describes the mixed
 503edge-kind case.  §4's failing schedule on `twoBridges` is a witness of a different family: its
 504imbalance is `1` on one edge letter and `0` on the other, not the incidence imbalance. -/
 505theorem dynamics_produces_incidence_countermodel {B : ℕ} (K : BoundedComplex B)
 506    (magv : PostingAlphabet K → ℝ) (hnn : ∀ a, 0 ≤ magv a) :
 507    ∃ (L : Recognition.Ledger (discreteCarrier (PostingAlphabet K))),
 508      PostReachable zeroLedger L ∧
 509      ∃ S : DualEntryStrainState (PostingAlphabet K),
 510        S.phi = incidenceImbalance K ∧ S.mag = magv := by
 511  obtain ⟨L, _, hreach, hphi⟩ := imbalance_realized (incidenceImbalance K)
 512  refine ⟨L, hreach, ?_⟩
 513  have hflux : ∀ i, |Recognition.phi L i| ≤ 1 := by
 514    intro i
 515    have hi := congrFun hphi i
 516    rw [hi]
 517    cases i with
 518    | inl v => simp [incidenceImbalance]
 519    | inr rest =>
 520      cases rest with
 521      | inl e =>
 522        by_cases h : (K.edgeVerts e).1 ≠ (K.edgeVerts e).2
 523        · simp [incidenceImbalance, h]
 524        · simp [incidenceImbalance, h]
 525      | inr t => simp [incidenceImbalance]
 526  refine ⟨DualEntryStrainState.ofLedger L magv hnn hflux, ?_, rfl⟩
 527  show (DualEntryStrainState.ofLedger L magv hnn hflux).phi = incidenceImbalance K
 528  rw [DualEntryStrainState.phi_ofLedger L magv hnn hflux]
 529  exact hphi
 530
 531/-! ## §4. The premise, named at the only layer where it can live: the schedule -/
 532
 533/-- An imbalance configuration is counts-only (kind-constant) on a complex's posting alphabet:
 534constant on vertex letters, constant on edge letters, constant on tetrahedron letters.  This is
 535the imbalance-level content of the third arc's `ChargesCountsOnly`, stated directly on the
 536charge the dynamics produces. -/
 537def CountsOnlyImbalance {B : ℕ} (K : BoundedComplex B) (χ : PostingAlphabet K → ℤ) : Prop :=
 538  ∃ cV cE cT : ℤ,
 539    (∀ v : Fin K.nV, χ (Sum.inl v) = cV) ∧
 540    (∀ e : Fin K.nE, χ (Sum.inr (Sum.inl e)) = cE) ∧
 541    (∀ t : Fin K.nT, χ (Sum.inr (Sum.inr t)) = cT)
 542
 543/-- **The named premise, at the dynamics layer.**  A posting schedule is counts-only if the
 544imbalance it produces from balance is kind-constant at every tick.  Three arcs have now shown
 545that nothing below this premise forces it: not the cost-function space, not the lattice state
 546type, and not the dynamics, which reaches every imbalance.  What remains is exactly this: a law
 547about the actual schedule the universe executes.  It is a physical premise about one run, not
 548a theorem about the space of runs, and the countermodel below shows it is not forced. -/
 549def CountsOnlySchedule {B : ℕ} (K : BoundedComplex B) (sched : Schedule (PostingAlphabet K)) :
 550    Prop :=
 551  ∀ t : ℕ, CountsOnlyImbalance K (phiAfter sched t)
 552
 553/-- The posted letter of the countermodel schedule: edge 0 of the two-bridge witness. -/
 554def cmEdge0 : PostingAlphabet twoBridges := Sum.inr (Sum.inl ⟨0, by decide⟩)
 555
 556/-- The other edge letter of the two-bridge witness. -/
 557def cmEdge1 : PostingAlphabet twoBridges := Sum.inr (Sum.inl ⟨1, by decide⟩)
 558
 559theorem cmEdge1_ne_cmEdge0 : cmEdge1 ≠ cmEdge0 := by
 560  intro hh
 561  have h2 := Sum.inr.inj hh
 562  have h3 := Sum.inl.inj h2
 563  exact absurd h3 (by decide)
 564
 565/-- The one-post countermodel schedule on the two-bridge witness: a single debit on edge
 566letter 0 at tick 0, idle forever after.  It is a legal run of the posting dynamics. -/
 567def countermodelSchedule : Schedule (PostingAlphabet twoBridges)
 568  | 0 => some (cmEdge0, .debit)
 569  | _ => none
 570
 571/-- **THEOREM (the premise is not forced by the dynamics).**  The countermodel schedule's
 572imbalance after one tick is `1` on edge letter 0 and `0` on edge letter 1, two letters of the
 573same kind.  So a legal run of the posting dynamics produces a not-counts-only charge: no
 574counts-only law about schedules is derivable from the dynamics. -/
 575theorem schedule_countermodel_not_countsOnly :
 576    ¬ CountsOnlySchedule twoBridges countermodelSchedule := by
 577  intro h
 578  obtain ⟨_, cE, _, _, hE, _⟩ := h 1
 579  have hr : runSchedule zeroLedger countermodelSchedule 1
 580      = postAt zeroLedger cmEdge0 .debit := by
 581    simp only [runSchedule, countermodelSchedule]
 582  have h0 : phiAfter countermodelSchedule 1 cmEdge0 = 1 := by
 583    show Recognition.phi (runSchedule zeroLedger countermodelSchedule 1) cmEdge0 = 1
 584    rw [hr, phi_postAt_debit_self, phi_zeroLedger]
 585    omega
 586  have h1 : phiAfter countermodelSchedule 1 cmEdge1 = 0 := by
 587    show Recognition.phi (runSchedule zeroLedger countermodelSchedule 1) cmEdge1 = 0
 588    rw [hr, phi_postAt_ne zeroLedger cmEdge1_ne_cmEdge0 .debit, phi_zeroLedger]
 589  have hcontra : (1 : ℤ) = 0 := by
 590    calc (1 : ℤ) = phiAfter countermodelSchedule 1 cmEdge0 := h0.symm
 591      _ = cE := hE ⟨0, by decide⟩
 592      _ = phiAfter countermodelSchedule 1 cmEdge1 := (hE ⟨1, by decide⟩).symm
 593      _ = 0 := h1
 594  exact one_ne_zero hcontra
 595
 596/-! ## §5. The three-layer verdict, the index, and what the measure track gets -/
 597
 598/-- **THEOREM (the ledger forces counts-only at no layer examined).**  The conjunction of the
 599three arcs' negative results: the letter-cost space admits a not-counts-only charge (third
 600arc), the lattice state type admits a not-counts-only induced charge (fourth arc), and the
 601posting dynamics runs to a not-counts-only imbalance from balance (this arc).  Counts-only is
 602therefore not forced at any of these three named layers.  Whether a deeper layer than the
 603posting step exists and could force it is outside what this theorem says: the library carries
 604no such layer, and the remaining live form of the premise is a law about the actual schedule,
 605`CountsOnlySchedule`, whose satisfaction by nature's run is a physical premise rather than a
 606theorem about the space of runs. -/
 607theorem ledger_forces_countsOnly_at_no_layer :
 608    (¬ ChargesCountsOnly (incidenceCost 1)) ∧
 609    (¬ ChargesCountsOnly (incidencePhiLattice.toLetterCost)) ∧
 610    (∃ (sched : Schedule (PostingAlphabet twoBridges)),
 611      ¬ CountsOnlySchedule twoBridges sched) :=
 612  ⟨chargesCountsOnly_excludes_incidence 1 one_ne_zero,
 613   incidencePhiLattice_not_countsOnly,
 614   ⟨countermodelSchedule, schedule_countermodel_not_countsOnly⟩⟩
 615
 616/-- The index of the fifth arc.  Each flag is the Prop form of the corresponding theorem, so
 617`index_audit` pins them together.  The fourth flag is the premise in its strongest schedule
 618form: "every posting schedule on the two-bridge witness is counts-only."  The audit refutes
 619that Prop with the exhibited countermodel schedule, so the negative in the index is a real
 620theorem, not a constant. -/
 621structure Index where
 622  dynamics_reaches_every_nonneg_ledger : Prop
 623  every_imbalance_realized_by_schedule : Prop
 624  dynamics_produces_incidence_countermodel : Prop
 625  dynamics_forces_countsOnly_schedule : Prop
 626  premise_named_at : String
 627
 628def index : Index where
 629  dynamics_reaches_every_nonneg_ledger :=
 630    ∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ] (L : Recognition.Ledger (discreteCarrier Λ)),
 631      (∀ i, 0 ≤ L.debit i ∧ 0 ≤ L.credit i) → PostReachable zeroLedger L
 632  every_imbalance_realized_by_schedule :=
 633    ∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ] (φ : Λ → ℤ),
 634      ∃ (sched : Schedule Λ) (t : ℕ), phiAfter sched t = φ
 635  dynamics_produces_incidence_countermodel :=
 636    ∀ {B : ℕ} (K : BoundedComplex B) (magv : PostingAlphabet K → ℝ) (hnn : ∀ a, 0 ≤ magv a),
 637      ∃ (L : Recognition.Ledger (discreteCarrier (PostingAlphabet K))),
 638        PostReachable zeroLedger L ∧
 639        ∃ S : DualEntryStrainState (PostingAlphabet K),
 640          S.phi = incidenceImbalance K ∧ S.mag = magv
 641  dynamics_forces_countsOnly_schedule :=
 642    ∀ sched : Schedule (PostingAlphabet twoBridges), CountsOnlySchedule twoBridges sched
 643  premise_named_at := "CountsOnlySchedule: a law about the actual posting run, not derivable"
 644
 645/-- The audit pinning the index flags to their theorems.  The fourth conjunct refutes the
 646universal schedule law using the one-post countermodel of §4. -/
 647theorem index_audit : index.dynamics_reaches_every_nonneg_ledger ∧
 648    index.every_imbalance_realized_by_schedule ∧
 649    index.dynamics_produces_incidence_countermodel ∧
 650    ¬ index.dynamics_forces_countsOnly_schedule := by
 651  refine ⟨?_, ?_, ?_, ?_⟩
 652  · intro Λ _ _ L hnn
 653    exact postReachable_zero_of_nonneg (mass L) L (Nat.le_refl _) hnn
 654  · intro Λ _ _ φ
 655    exact imbalance_realized_by_schedule φ
 656  · intro B K magv hnn
 657    exact dynamics_produces_incidence_countermodel K magv hnn
 658  · intro h
 659    exact schedule_countermodel_not_countsOnly (h countermodelSchedule)
 660
 661end
 662
 663#print axioms postReachable_zero_of_nonneg
 664#print axioms imbalance_realized
 665#print axioms imbalance_realized_by_schedule
 666#print axioms dynamics_produces_incidence_countermodel
 667#print axioms schedule_countermodel_not_countsOnly
 668#print axioms ledger_forces_countsOnly_at_no_layer
 669#print axioms index_audit
 670
 671end Gap2DynamicsKindRule
 672end SevenGaps
 673end Gravity
 674end IndisputableMonolith
 675