import Sal.ConditionedMRDTs.MRDT_Instances.EmbedRGA.EmbedRGA_AnchorsFactor
import Sal.MRDTs.RGA_Embed.Embed_Code_EliasDelta

/-!
# `compactEliasDelta`: the concrete verified compaction

The compaction for the embed RGA, as a `StablePrefixMap` producer:

* **(a) DROP dead ranges**, `ePruneKeep`: a stable chain is carried forward
  iff it has a live descendant in the stable tree or a known in-flight
  coordinate passes through it; everything else is dropped, and its sibling
  rank is reclaimed.
* **(b) RANK-RENUMBER**, `rED`: in each sibling group with **no known
  in-flight child delta** (`skipAt = false`), the surviving deltas are
  renumbered to `1..k` order-isomorphically (`rankIn`) and re-encoded with
  the same ordered prefix code; groups *with* in-flight children are skipped
  this epoch. Spine fusion for such groups is a separate construction
  (`EmbedRGA_Fusion.lean`).

Soundness: H2 (`ord`) is `remapChain_keyLt`, per-group order-isomorphism
composed through the chain-lex theorem (`chainBefore_display`, where the
code's monotonicity lives); the rank map is an order-isomorphism against
surviving kids and is dominated by Lamport-fresh future deltas (`rED_iso`);
H3 (`ext`) holds by construction (the re-map rewrites the stable chain
prefix wholesale and never touches the minted delta codeword); H1 is derived
by the bundle. The headline (`compactRanked_settled_reads`,
`compactEliasDelta_settled_reads`) discharges everything at a `SettledAtOn`
cut of a disciplined honest configuration: freshness comes from
`Configuration.causal_mono` (the Lamport clause) through
`settledAt_dichotomy`.

**Addressing (runtime-twin erratum honored):** the cut-side inputs `tree`,
`live`, `inflight` are lists of *chains* (coordinate-addressed data), never
event ids resolved through prefix sums; id arithmetic appears only inside
the epoch-zero honest configuration. Scope: the **single-epoch** statement,
one compaction at a settled cut of an honest configuration.
-/

namespace Sal.ConditionedMRDTs

open Sal.Emulation
open Sal.EmbedRGA (OrderedPrefixCode PosChain coordOf coordOf_append
  coordOf_inj key keyLt keyLt_irrefl keyLt_asymm chainBefore chainBefore_total
  chainBefore_display enc_ne_nil eliasDeltaCode)

set_option linter.unusedSectionVars false

variable {α : Type} [DecidableEq α] [Inhabited α]

/-! ## §1 Chain-prefix alignment: bit prefixes of coordinates ARE chain
prefixes (prefix-freedom decodes the cut point onto a codeword boundary) -/

theorem coordOf_prefix_align (Γ : OrderedPrefixCode) :
    ∀ {ch1 ch2 : List ℕ}, PosChain ch1 → PosChain ch2 →
      coordOf Γ ch1 <+: coordOf Γ ch2 → ch1 <+: ch2
  | [], _, _, _, _ => List.nil_prefix
  | d :: ds, [], h1, _, h => by
      exfalso
      have hnil : coordOf Γ (d :: ds) = [] := List.prefix_nil.mp h
      simp only [coordOf] at hnil
      cases henc : Γ.enc d with
      | nil => exact enc_ne_nil Γ (h1 d List.mem_cons_self) henc
      | cons b bs => rw [henc] at hnil; simp at hnil
  | d :: ds, e :: es, h1, h2, h => by
      simp only [coordOf] at h
      have hd1 : 1 ≤ d := h1 d List.mem_cons_self
      have he1 : 1 ≤ e := h2 e List.mem_cons_self
      have hde : d = e := by
        by_contra hne
        have p1 : Γ.enc d <+: Γ.enc e ++ coordOf Γ es :=
          List.IsPrefix.trans (List.prefix_append _ _) h
        have p2 : Γ.enc e <+: Γ.enc e ++ coordOf Γ es := List.prefix_append _ _
        rcases Nat.le_total (Γ.enc d).length (Γ.enc e).length with hle | hle
        · exact Γ.prefixFree hd1 he1 hne
            (List.prefix_of_prefix_length_le p1 p2 hle)
        · exact Γ.prefixFree he1 hd1 (Ne.symm hne)
            (List.prefix_of_prefix_length_le p2 p1 hle)
      subst hde
      have htail : coordOf Γ ds <+: coordOf Γ es := by
        obtain ⟨w, hw⟩ := h
        rw [List.append_assoc] at hw
        exact ⟨w, List.append_cancel_left hw⟩
      exact List.cons_prefix_cons.mpr ⟨rfl,
        coordOf_prefix_align Γ
          (fun x hx => h1 x (List.mem_cons_of_mem _ hx))
          (fun x hx => h2 x (List.mem_cons_of_mem _ hx)) htail⟩

theorem coordOf_prefix_of_prefix (Γ : OrderedPrefixCode) {ch1 ch2 : List ℕ}
    (h : ch1 <+: ch2) : coordOf Γ ch1 <+: coordOf Γ ch2 := by
  obtain ⟨u, hu⟩ := h
  exact ⟨coordOf Γ u, by rw [← coordOf_append, hu]⟩

theorem prefix_snoc_cons (p : List ℕ) (d : ℕ) (c : List ℕ) :
    (p ++ [d]) <+: (p ++ d :: c) := by
  have h := List.prefix_append (p ++ [d]) c
  rwa [List.append_assoc, List.singleton_append] at h

/-! ## §2 The chain re-map: per-position renumbering keyed on the (old)
parent prefix -/

/-- Re-map a chain suffix, the accumulator carrying the original parent
prefix: position `i`'s delta `d` under parent `p` becomes `r p d`. -/
def remapFrom (r : List ℕ → ℕ → ℕ) : List ℕ → List ℕ → List ℕ
  | _, [] => []
  | p, d :: ds => r p d :: remapFrom r (p ++ [d]) ds

/-- The whole-chain re-map. -/
def remapChain (r : List ℕ → ℕ → ℕ) (ch : List ℕ) : List ℕ :=
  remapFrom r [] ch

theorem remapFrom_cons (r : List ℕ → ℕ → ℕ) (p : List ℕ) (d : ℕ)
    (ds : List ℕ) :
    remapFrom r p (d :: ds) = r p d :: remapFrom r (p ++ [d]) ds := rfl

theorem remapFrom_length (r : List ℕ → ℕ → ℕ) :
    ∀ (ds p : List ℕ), (remapFrom r p ds).length = ds.length
  | [], _ => rfl
  | d :: ds, p => by
      rw [remapFrom_cons, List.length_cons, List.length_cons,
        remapFrom_length r ds]

theorem remapFrom_append (r : List ℕ → ℕ → ℕ) :
    ∀ (u p v : List ℕ),
      remapFrom r p (u ++ v) = remapFrom r p u ++ remapFrom r (p ++ u) v
  | [], p, v => by simp [remapFrom]
  | d :: u', p, v => by
      simp only [List.cons_append, remapFrom_cons]
      rw [remapFrom_append r u' (p ++ [d]) v]
      simp [List.append_assoc]

theorem remapFrom_pos {r : List ℕ → ℕ → ℕ}
    (hr : ∀ p d, 1 ≤ d → 1 ≤ r p d) :
    ∀ (ds p : List ℕ), PosChain ds → PosChain (remapFrom r p ds)
  | [], _, _ => fun x hx => absurd hx (List.not_mem_nil)
  | d :: ds, p, h => by
      intro x hx
      rw [remapFrom_cons] at hx
      rcases List.mem_cons.mp hx with rfl | hx'
      · exact hr p d (h d List.mem_cons_self)
      · exact remapFrom_pos hr ds (p ++ [d])
          (fun y hy => h y (List.mem_cons_of_mem _ hy)) x hx'

/-- Off the kept tree the re-map is the identity, position for position. -/
theorem remapFrom_id {keep : List (List ℕ)} {r : List ℕ → ℕ → ℕ}
    (hrOff : ∀ p d, (p ++ [d]) ∉ keep → r p d = d) :
    ∀ (u p : List ℕ),
      (∀ q e, (q ++ [e]) <+: u → (p ++ q ++ [e]) ∉ keep) →
      remapFrom r p u = u
  | [], _, _ => rfl
  | x :: xs, p, h => by
      rw [remapFrom_cons]
      have hx : r p x = x := by
        apply hrOff
        have := h [] x (by simp)
        simpa using this
      have htail := remapFrom_id hrOff xs (p ++ [x]) (fun q e hqe => by
        have h2 := h (x :: q) e (by
          rw [show (x :: q) ++ [e] = x :: (q ++ [e]) from rfl]
          exact List.cons_prefix_cons.mpr ⟨rfl, hqe⟩)
        simpa [List.append_assoc] using h2)
      rw [hx, htail]

/-! ## §3 H2, generically: an order-isomorphic per-group renumbering
preserves the display comparator (through the chain-lex theorem, this is
where the code's monotonicity is consumed) -/

/-- `(p, d)` occurs in the domain: some at-hand chain passes through the
node `p ++ [d]`. -/
def Occ (𝒟 : List ℕ → Prop) (p : List ℕ) (d : ℕ) : Prop :=
  ∃ ch, 𝒟 ch ∧ (p ++ [d]) <+: ch

theorem remapChain_chainBefore {r : List ℕ → ℕ → ℕ} {𝒟 : List ℕ → Prop}
    (hiso : ∀ p d e, Occ 𝒟 p d → Occ 𝒟 p e → d < e → r p d < r p e)
    {ch ch' : List ℕ} (h : 𝒟 ch) (h' : 𝒟 ch') (hb : chainBefore ch ch') :
    chainBefore (remapChain r ch) (remapChain r ch') := by
  cases hb with
  | ancestor ch0 ext hne =>
      rw [remapChain, remapChain, remapFrom_append]
      refine chainBefore.ancestor _ _ (fun hnil => hne ?_)
      have hlen := congrArg List.length hnil
      rw [remapFrom_length] at hlen
      exact List.eq_nil_of_length_eq_zero hlen
  | newer p0 d e c1 c2 hlt =>
      have hoccd : Occ 𝒟 p0 d := ⟨p0 ++ d :: c1, h, prefix_snoc_cons p0 d c1⟩
      have hocce : Occ 𝒟 p0 e := ⟨p0 ++ e :: c2, h', prefix_snoc_cons p0 e c2⟩
      have hred : r p0 e < r p0 d := hiso p0 e d hocce hoccd hlt
      have e1 : remapChain r (p0 ++ d :: c1)
          = remapFrom r [] p0 ++ r p0 d :: remapFrom r (p0 ++ [d]) c1 := by
        rw [remapChain, show p0 ++ d :: c1 = (p0 ++ [d]) ++ c1 from by simp,
          remapFrom_append, remapFrom_append]
        simp [remapFrom, List.append_assoc]
      have e2 : remapChain r (p0 ++ e :: c2)
          = remapFrom r [] p0 ++ r p0 e :: remapFrom r (p0 ++ [e]) c2 := by
        rw [remapChain, show p0 ++ e :: c2 = (p0 ++ [e]) ++ c2 from by simp,
          remapFrom_append, remapFrom_append]
        simp [remapFrom, List.append_assoc]
      rw [e1, e2]
      exact chainBefore.newer _ _ _ _ _ hred

/-- **H2, the generic soundness theorem**: an order-isomorphic (on occurring
sibling pairs), positivity-preserving chain re-map preserves the fold's key
comparator, as a Boolean equation (both directions). -/
theorem remapChain_keyLt (Γ : OrderedPrefixCode) {r : List ℕ → ℕ → ℕ}
    {𝒟 : List ℕ → Prop} (hDpos : ∀ ch, 𝒟 ch → PosChain ch)
    (hrPos : ∀ p d, 1 ≤ d → 1 ≤ r p d)
    (hiso : ∀ p d e, Occ 𝒟 p d → Occ 𝒟 p e → d < e → r p d < r p e)
    {ch ch' : List ℕ} (h : 𝒟 ch) (h' : 𝒟 ch') :
    keyLt (key (coordOf Γ (remapChain r ch)))
        (key (coordOf Γ (remapChain r ch')))
      = keyLt (key (coordOf Γ ch)) (key (coordOf Γ ch')) := by
  by_cases heq : ch = ch'
  · subst heq
    rw [keyLt_irrefl, keyLt_irrefl]
  · have hpos := hDpos ch h
    have hpos' := hDpos ch' h'
    have hrp : PosChain (remapChain r ch) := remapFrom_pos hrPos ch [] hpos
    have hrp' : PosChain (remapChain r ch') := remapFrom_pos hrPos ch' [] hpos'
    rcases chainBefore_total heq with hb | hb
    · have h1 := chainBefore_display Γ hpos hpos' hb
      have h2 := chainBefore_display Γ hrp hrp'
        (remapChain_chainBefore hiso h h' hb)
      rw [keyLt_asymm h1, keyLt_asymm h2]
    · have h1 := chainBefore_display Γ hpos' hpos hb
      have h2 := chainBefore_display Γ hrp' hrp
        (remapChain_chainBefore hiso h' h hb)
      rw [h1, h2]

/-! ## §4 The induced bit-string translation: longest kept stable prefix
rewritten wholesale, tail verbatim -/

/-- The longest kept chain whose coordinate prefixes `c` (`[]` if none). -/
def stabChain (Γ : OrderedPrefixCode) : List (List ℕ) → List Bool → List ℕ
  | [], _ => []
  | k :: ks, c =>
      if (coordOf Γ k).isPrefixOf c ∧ (stabChain Γ ks c).length < k.length
      then k else stabChain Γ ks c

theorem stabChain_spec (Γ : OrderedPrefixCode) :
    ∀ (K : List (List ℕ)) (c : List Bool),
      stabChain Γ K c = [] ∨
        (stabChain Γ K c ∈ K ∧ coordOf Γ (stabChain Γ K c) <+: c)
  | [], _ => Or.inl rfl
  | k :: ks, c => by
      simp only [stabChain]
      by_cases h : (coordOf Γ k).isPrefixOf c
          ∧ (stabChain Γ ks c).length < k.length
      · rw [if_pos h]
        exact Or.inr ⟨List.mem_cons_self, List.isPrefixOf_iff_prefix.mp h.1⟩
      · rw [if_neg h]
        rcases stabChain_spec Γ ks c with h' | ⟨hm, hp⟩
        · exact Or.inl h'
        · exact Or.inr ⟨List.mem_cons_of_mem _ hm, hp⟩

theorem stabChain_max (Γ : OrderedPrefixCode) :
    ∀ (K : List (List ℕ)) (c : List Bool) (k : List ℕ), k ∈ K →
      coordOf Γ k <+: c → k.length ≤ (stabChain Γ K c).length
  | [], _, _, hk, _ => absurd hk (List.not_mem_nil)
  | k0 :: ks, c, k, hk, hp => by
      simp only [stabChain]
      by_cases h : (coordOf Γ k0).isPrefixOf c
          ∧ (stabChain Γ ks c).length < k0.length
      · rw [if_pos h]
        rcases List.mem_cons.mp hk with rfl | hk'
        · exact Nat.le_refl _
        · exact Nat.le_trans (stabChain_max Γ ks c k hk' hp) (Nat.le_of_lt h.2)
      · rw [if_neg h]
        rcases List.mem_cons.mp hk with rfl | hk'
        · rcases Nat.lt_or_ge (stabChain Γ ks c).length k.length with hlt | hge
          · exact absurd ⟨List.isPrefixOf_iff_prefix.mpr hp, hlt⟩ h
          · exact hge
        · exact stabChain_max Γ ks c k hk' hp

/-- **The lazy translation, concretely**: rewrite the longest kept stable
prefix through the chain re-map, keep the tail bit-for-bit. Total and
computable on all bit strings. -/
def fStab (Γ : OrderedPrefixCode) (r : List ℕ → ℕ → ℕ)
    (keep : List (List ℕ)) (c : List Bool) : List Bool :=
  coordOf Γ (remapChain r (stabChain Γ keep c))
    ++ c.drop (coordOf Γ (stabChain Γ keep c)).length

/-- **The master alignment lemma**: on any positive chain's coordinate the
bit-string translation IS the chain re-map, the stable/unstable split lands
on a codeword boundary and the tail is off the kept tree, where `r` is the
identity. No domain hypothesis: this holds for every positive chain. -/
theorem fStab_coordOf (Γ : OrderedPrefixCode) {r : List ℕ → ℕ → ℕ}
    {keep : List (List ℕ)} (hKpos : ∀ k ∈ keep, PosChain k)
    (hrOff : ∀ p d, (p ++ [d]) ∉ keep → r p d = d)
    {ch : List ℕ} (hch : PosChain ch) :
    fStab Γ r keep (coordOf Γ ch) = coordOf Γ (remapChain r ch) := by
  rcases stabChain_spec Γ keep (coordOf Γ ch) with hnil | ⟨hmem, hpre⟩
  · have hid : remapChain r ch = ch := by
      apply remapFrom_id hrOff
      intro q e hqe hin
      have hin' : (q ++ [e]) ∈ keep := by simpa using hin
      have hmax := stabChain_max Γ keep (coordOf Γ ch) _ hin'
        (coordOf_prefix_of_prefix Γ hqe)
      rw [hnil] at hmax
      simp at hmax
    rw [fStab, hnil, hid]
    simp [remapChain, remapFrom, coordOf]
  · have hspos : PosChain (stabChain Γ keep (coordOf Γ ch)) := hKpos _ hmem
    have hsch : stabChain Γ keep (coordOf Γ ch) <+: ch :=
      coordOf_prefix_align Γ hspos hch hpre
    set st := stabChain Γ keep (coordOf Γ ch) with hst
    obtain ⟨u, hu⟩ := hsch
    have htail : remapFrom r st u = u := by
      apply remapFrom_id hrOff
      intro q e hqe hin
      have hpre2 : ((st ++ q) ++ [e]) <+: ch := by
        obtain ⟨w, hw⟩ := hqe
        refine ⟨w, ?_⟩
        rw [← hu, List.append_assoc, List.append_assoc]
        congr 1
        rw [← List.append_assoc]
        exact hw
      have hmax := stabChain_max Γ keep (coordOf Γ ch) _ hin
        (coordOf_prefix_of_prefix Γ hpre2)
      rw [← hst] at hmax
      simp only [List.length_append, List.length_singleton] at hmax
      omega
    rw [fStab, ← hst, ← hu, coordOf_append, List.drop_left]
    simp only [remapChain, remapFrom_append, List.nil_append, htail,
      coordOf_append]

/-! ## §5 The bundle producer: H3 by construction, H2 by §3, H1 derived -/

/-- The at-rest domain: coordinates of at-hand chains. -/
def compactRest (Γ : OrderedPrefixCode) (𝒟 : List ℕ → Prop)
    (c : List Bool) : Prop :=
  ∃ ch, 𝒟 ch ∧ c = coordOf Γ ch

/-- The mint domain: one fresh positive delta on an at-hand anchor chain,
the minted node off the kept tree (it is a new-epoch node). -/
def compactMintAt (Γ : OrderedPrefixCode) (keep : List (List ℕ))
    (𝒟 : List ℕ → Prop) (π : List Bool) (δ : ℕ) : Prop :=
  1 ≤ δ ∧ ∃ chA, π = coordOf Γ chA ∧ PosChain chA ∧ 𝒟 (chA ++ [δ]) ∧
    (chA ++ [δ]) ∉ keep

theorem compactDom_chain {Γ : OrderedPrefixCode} {keep : List (List ℕ)}
    {𝒟 : List ℕ → Prop} {c : List Bool}
    (h : compactRest Γ 𝒟 c ∨
      ∃ π δ, compactMintAt Γ keep 𝒟 π δ ∧ c = π ++ Γ.enc δ) :
    ∃ ch, 𝒟 ch ∧ c = coordOf Γ ch := by
  rcases h with ⟨ch, hch, rfl⟩ | ⟨π, δ, ⟨hδ, chA, rfl, hpos, hD, -⟩, rfl⟩
  · exact ⟨ch, hch, rfl⟩
  · exact ⟨chA ++ [δ], hD, by rw [coordOf_append]; simp [coordOf]⟩

/-- **The generic compaction bundle**: any renumbering that is positive,
identity off the kept tree, and order-isomorphic on occurring sibling pairs
induces a `StablePrefixMap` through the longest-kept-prefix translation. -/
def compactSPM (Γ : OrderedPrefixCode) (keep : List (List ℕ))
    (r : List ℕ → ℕ → ℕ) (𝒟 : List ℕ → Prop)
    (hKpos : ∀ k ∈ keep, PosChain k)
    (hDpos : ∀ ch, 𝒟 ch → PosChain ch)
    (hrPos : ∀ p d, 1 ≤ d → 1 ≤ r p d)
    (hrOff : ∀ p d, (p ++ [d]) ∉ keep → r p d = d)
    (hiso : ∀ p d e, Occ 𝒟 p d → Occ 𝒟 p e → d < e → r p d < r p e) :
    StablePrefixMap Γ where
  f := fStab Γ r keep
  Rest := compactRest Γ 𝒟
  MintAt := compactMintAt Γ keep 𝒟
  ext := by
    rintro π δ ⟨hδ, chA, rfl, hpos, hD, hnk⟩
    have hposm : PosChain (chA ++ [δ]) := hDpos _ hD
    have hcoord : coordOf Γ chA ++ Γ.enc δ = coordOf Γ (chA ++ [δ]) := by
      rw [coordOf_append]
      simp [coordOf]
    have hrm : remapChain r (chA ++ [δ]) = remapChain r chA ++ [δ] := by
      simp only [remapChain]
      rw [remapFrom_append, List.nil_append, remapFrom_cons,
        hrOff chA δ hnk]
      rfl
    rw [hcoord, fStab_coordOf Γ hKpos hrOff hposm,
      fStab_coordOf Γ hKpos hrOff hpos, hrm, coordOf_append]
    congr 1
    simp [coordOf]
  ord := by
    intro c c' h h'
    obtain ⟨ch, hch, rfl⟩ := compactDom_chain h
    obtain ⟨ch', hch', rfl⟩ := compactDom_chain h'
    rw [fStab_coordOf Γ hKpos hrOff (hDpos _ hch),
      fStab_coordOf Γ hKpos hrOff (hDpos _ hch')]
    exact remapChain_keyLt Γ hDpos hrPos hiso hch hch'

/-! ## §6 The concrete renumbering: drop dead ranges, rank-renumber
in-flight-free sibling groups -/

/-- The child deltas of `p` recorded in a chain list. -/
def kidsOf (K : List (List ℕ)) (p : List ℕ) : List ℕ :=
  K.filterMap (fun k => if k.dropLast = p then k.getLast? else none)

theorem mem_kidsOf {K : List (List ℕ)} {p : List ℕ} {d : ℕ} :
    d ∈ kidsOf K p ↔ (p ++ [d]) ∈ K := by
  simp only [kidsOf, List.mem_filterMap]
  constructor
  · rintro ⟨k, hk, hsome⟩
    by_cases hdp : k.dropLast = p
    · rw [if_pos hdp] at hsome
      obtain ⟨l', rfl⟩ := List.getLast?_eq_some_iff.mp hsome
      rw [List.dropLast_concat] at hdp
      exact hdp ▸ hk
    · rw [if_neg hdp] at hsome
      exact absurd hsome (by simp)
  · intro hk
    exact ⟨p ++ [d], hk, by rw [if_pos (List.dropLast_concat), List.getLast?_concat]⟩

/-- The 1-based rank of `d` among the (deduplicated) deltas of a group. -/
def rankIn (ds : List ℕ) (d : ℕ) : ℕ :=
  (ds.dedup.filter (fun e => e ≤ d)).length

/-- Rank is strictly monotone against recorded deltas. -/
theorem rankIn_lt_rankIn {ds : List ℕ} {d e : ℕ} (hde : d < e)
    (he : e ∈ ds) : rankIn ds d < rankIn ds e := by
  have hsub : List.Sublist (ds.dedup.filter (fun a => a ≤ d))
      (ds.dedup.filter (fun a => a ≤ e)) := by
    apply List.monotone_filter_right
    intro a ha
    simp only [decide_eq_true_eq] at ha ⊢
    omega
  have hmem : e ∈ ds.dedup.filter (fun a => a ≤ e) :=
    List.mem_filter.mpr ⟨List.mem_dedup.mpr he, by simp⟩
  have hnmem : e ∉ ds.dedup.filter (fun a => a ≤ d) := by
    intro hmem'
    have := (List.mem_filter.mp hmem').2
    simp only [decide_eq_true_eq] at this
    omega
  refine Nat.lt_of_le_of_ne hsub.length_le (fun heq => ?_)
  have heql := hsub.eq_of_length heq
  rw [← heql] at hmem
  exact hnmem hmem

/-- A duplicate-free list of integers in `[1, d]` has at most `d` members. -/
theorem nodup_length_le_of_bounded :
    ∀ (d : ℕ) (l : List ℕ), l.Nodup → (∀ x ∈ l, 1 ≤ x ∧ x ≤ d) →
      l.length ≤ d
  | 0, [], _, _ => Nat.le_refl _
  | 0, x :: xs, _, hb => by
      obtain ⟨h1, h2⟩ := hb x List.mem_cons_self
      omega
  | d + 1, l, hnd, hb => by
      by_cases hmem : (d + 1) ∈ l
      · have hlen := List.length_erase_of_mem hmem
        have hle := nodup_length_le_of_bounded d (l.erase (d + 1))
          (hnd.erase _) (fun x hx => by
            have hx' := (hnd.mem_erase_iff).mp hx
            obtain ⟨h1, h2⟩ := hb x hx'.2
            have := hx'.1
            omega)
        have hpos : 1 ≤ l.length := by
          cases l with
          | nil => exact absurd hmem (List.not_mem_nil)
          | cons y ys => simp
        omega
      · have hle := nodup_length_le_of_bounded d l hnd (fun x hx => by
          obtain ⟨h1, h2⟩ := hb x hx
          rcases Nat.lt_or_ge x (d + 1) with h | h
          · omega
          · exact absurd (Nat.le_antisymm h2 h ▸ hx) hmem)
        omega

/-- Rank never exceeds the delta it renumbers (distinct positives below `d`
number at most `d`), the freshness-domination half of H2. -/
theorem rankIn_le_self {ds : List ℕ} (hpos : ∀ x ∈ ds, 1 ≤ x) (d : ℕ) :
    rankIn ds d ≤ d := by
  apply nodup_length_le_of_bounded d _ ((List.nodup_dedup ds).filter _)
  intro x hx
  obtain ⟨hx1, hx2⟩ := List.mem_filter.mp hx
  simp only [decide_eq_true_eq] at hx2
  exact ⟨hpos x (List.mem_dedup.mp hx1), hx2⟩

/-- Group `p` has a known in-flight child delta. -/
def skipAt (inflight : List (List ℕ)) (p : List ℕ) : Bool :=
  !(kidsOf inflight p).isEmpty

theorem skipAt_eq_false {inflight : List (List ℕ)} {p : List ℕ} :
    skipAt inflight p = false ↔ ∀ d, (p ++ [d]) ∉ inflight := by
  constructor
  · intro h d hd
    have hmem : d ∈ kidsOf inflight p := mem_kidsOf.mpr hd
    have : kidsOf inflight p ≠ [] := List.ne_nil_of_mem hmem
    simp only [skipAt, Bool.not_eq_false', List.isEmpty_iff] at h
    exact this h
  · intro h
    simp only [skipAt, Bool.not_eq_false', List.isEmpty_iff]
    cases hk : kidsOf inflight p with
    | nil => rfl
    | cons x xs =>
        have hx : x ∈ kidsOf inflight p := by
          rw [hk]
          exact List.mem_cons_self
        exact absurd (mem_kidsOf.mp hx) (h x)

/-- **(a) DROP dead ranges**: carry a stable chain forward iff it has a live
descendant in the tree or a known in-flight coordinate passes through it. -/
def ePruneKeep (tree : List (List ℕ)) (live : List ℕ → Bool)
    (inflight : List (List ℕ)) : List (List ℕ) :=
  tree.filter (fun k =>
    tree.any (fun k' => k.isPrefixOf k' && live k') ||
    inflight.any (fun q => k.isPrefixOf q))

theorem mem_ePruneKeep {tree : List (List ℕ)} {live : List ℕ → Bool}
    {inflight : List (List ℕ)} {k : List ℕ} :
    k ∈ ePruneKeep tree live inflight ↔
      k ∈ tree ∧ ((∃ k' ∈ tree, k <+: k' ∧ live k' = true) ∨
        ∃ q ∈ inflight, k <+: q) := by
  simp [ePruneKeep, List.mem_filter, List.any_eq_true,
    List.isPrefixOf_iff_prefix, Bool.and_eq_true, Bool.or_eq_true]

theorem ePruneKeep_subset {tree : List (List ℕ)} {live : List ℕ → Bool}
    {inflight : List (List ℕ)} :
    ∀ k ∈ ePruneKeep tree live inflight, k ∈ tree :=
  fun _ hk => (mem_ePruneKeep.mp hk).1

theorem ePruneKeep_prefix {tree : List (List ℕ)} {live : List ℕ → Bool}
    {inflight : List (List ℕ)} {k1 k2 : List ℕ}
    (h12 : k1 <+: k2) (h2 : k2 ∈ ePruneKeep tree live inflight)
    (h1 : k1 ∈ tree) : k1 ∈ ePruneKeep tree live inflight := by
  rcases mem_ePruneKeep.mp h2 with ⟨-, ⟨k', hk', hp, hl⟩ | ⟨q, hq, hp⟩⟩
  · exact mem_ePruneKeep.mpr ⟨h1, Or.inl ⟨k', hk', h12.trans hp, hl⟩⟩
  · exact mem_ePruneKeep.mpr ⟨h1, Or.inr ⟨q, hq, h12.trans hp⟩⟩

/-- **(b) RANK-RENUMBER**: dense ranks in kept, in-flight-free sibling
groups; identity everywhere else (off-tree nodes, and groups with known
in-flight children, which are skipped). -/
def rED (keep : List (List ℕ)) (inflight : List (List ℕ))
    (p : List ℕ) (d : ℕ) : ℕ :=
  if (p ++ [d]) ∈ keep ∧ skipAt inflight p = false
  then rankIn (kidsOf keep p) d else d

theorem rED_off {keep inflight : List (List ℕ)} :
    ∀ p d, (p ++ [d]) ∉ keep → rED keep inflight p d = d := by
  intro p d h
  rw [rED, if_neg (fun hc => h hc.1)]

theorem rED_pos {keep inflight : List (List ℕ)} :
    ∀ p d, 1 ≤ d → 1 ≤ rED keep inflight p d := by
  intro p d hd
  rw [rED]
  split
  · next hc =>
      have hdk : d ∈ kidsOf keep p := mem_kidsOf.mpr hc.1
      have hmem : d ∈ (kidsOf keep p).dedup.filter (fun a => a ≤ d) :=
        List.mem_filter.mpr ⟨List.mem_dedup.mpr hdk, by simp⟩
      exact Nat.pos_of_ne_zero (fun h0 =>
        List.ne_nil_of_mem hmem (List.eq_nil_of_length_eq_zero h0))
  · exact hd

/-- **The stage-2 soundness theorem for the concrete renumbering** (per-group
order-isomorphism + Lamport freshness): if every occurring delta at an
unskipped group is a surviving kid or fresh (dominates every kid), `rED` is
strictly monotone on occurring sibling pairs, H2's hypothesis. -/
theorem rED_iso {keep inflight : List (List ℕ)} {𝒟 : List ℕ → Prop}
    (hKpos : ∀ k ∈ keep, PosChain k)
    (hocc : ∀ p d, Occ 𝒟 p d → skipAt inflight p = false →
      (p ++ [d]) ∈ keep ∨ ∀ e, (p ++ [e]) ∈ keep → e < d) :
    ∀ p d e, Occ 𝒟 p d → Occ 𝒟 p e → d < e →
      rED keep inflight p d < rED keep inflight p e := by
  intro p d e hd he hde
  by_cases hskip : skipAt inflight p = false
  · have hkids_pos : ∀ x ∈ kidsOf keep p, 1 ≤ x := by
      intro x hx
      exact hKpos _ (mem_kidsOf.mp hx) x
        (List.mem_append_right _ List.mem_cons_self)
    rcases hocc p d hd hskip with hkd | hfd
    · rcases hocc p e he hskip with hke | hfe
      · rw [rED, if_pos ⟨hkd, hskip⟩, rED, if_pos ⟨hke, hskip⟩]
        exact rankIn_lt_rankIn hde (mem_kidsOf.mpr hke)
      · have h1 : rED keep inflight p d = rankIn (kidsOf keep p) d := by
          rw [rED, if_pos ⟨hkd, hskip⟩]
        have h2 : rED keep inflight p e = e :=
          rED_off p e (fun hc => absurd (hfe e hc) (Nat.lt_irrefl e))
        rw [h1, h2]
        exact Nat.lt_of_le_of_lt (rankIn_le_self hkids_pos d) hde
    · rcases hocc p e he hskip with hke | hfe
      · exact absurd (hfd e hke) (Nat.lt_asymm hde)
      · rw [rED_off p d (fun hc => absurd (hfd d hc) (Nat.lt_irrefl d)),
          rED_off p e (fun hc => absurd (hfe e hc) (Nat.lt_irrefl e))]
        exact hde
  · rw [rED, if_neg (fun hc => hskip hc.2), rED, if_neg (fun hc => hskip hc.2)]
    exact hde

/-- The ranked compaction at any ordered prefix code, packaged as a
`StablePrefixMap`. -/
def compactRanked (Γ : OrderedPrefixCode) (tree : List (List ℕ))
    (live : List ℕ → Bool) (inflight : List (List ℕ)) (𝒟 : List ℕ → Prop)
    (htpos : ∀ k ∈ tree, PosChain k)
    (hDpos : ∀ ch, 𝒟 ch → PosChain ch)
    (hocc : ∀ p d, Occ 𝒟 p d → skipAt inflight p = false →
      (p ++ [d]) ∈ ePruneKeep tree live inflight ∨
      ∀ e, (p ++ [e]) ∈ ePruneKeep tree live inflight → e < d) :
    StablePrefixMap Γ :=
  compactSPM Γ (ePruneKeep tree live inflight)
    (rED (ePruneKeep tree live inflight) inflight) 𝒟
    (fun k hk => htpos k (ePruneKeep_subset k hk))
    hDpos
    (rED_pos)
    (rED_off)
    (rED_iso (fun k hk => htpos k (ePruneKeep_subset k hk)) hocc)

/-- **`compactEliasDelta`**, the concrete verified compaction: drop dead
ranges, rank-renumber in-flight-free sibling groups, re-encode with the
flipped Elias-δ code. -/
abbrev compactEliasDelta (tree : List (List ℕ)) (live : List ℕ → Bool)
    (inflight : List (List ℕ)) (𝒟 : List ℕ → Prop)
    (htpos : ∀ k ∈ tree, PosChain k)
    (hDpos : ∀ ch, 𝒟 ch → PosChain ch)
    (hocc : ∀ p d, Occ 𝒟 p d → skipAt inflight p = false →
      (p ++ [d]) ∈ ePruneKeep tree live inflight ∨
      ∀ e, (p ++ [e]) ∈ ePruneKeep tree live inflight → e < d) :
    StablePrefixMap eliasDeltaCode :=
  compactRanked eliasDeltaCode tree live inflight 𝒟 htpos hDpos hocc

/-- The at-hand chains of a settled cut: chains of cut-live settled inserts,
of known in-flight inserts, and of new-epoch (beyond-`Ev`) inserts, the
domain over which the compaction must preserve order. -/
def EAtHand (Γ : OrderedPrefixCode) (C : Configuration (E Γ α))
    (S Ev : Set (Op (EOp α))) (inflight : List (List ℕ))
    (chainOf : ℕ → List ℕ) (ch : List ℕ) : Prop :=
  ∃ o, o ∈ C.events ∧ eIsIns o = true ∧ chainOf o.1 = ch ∧
    ((o ∈ S ∧ ∀ dl ∈ Ev, dl.2.2 ≠ EOp.del o.1) ∨
      chainOf o.1 ∈ inflight ∨ o ∉ Ev)

/-! ## §7 The headline: at a settled cut of a disciplined honest
configuration, the ranked compaction preserves every read

Data adequacy (`hTree`/`hTreeS`/`hLive`/`hInflight`) is the protocol half's
obligation (recoding note §6), stated **coordinate-addressed** (chains
matched through `coordOf`, never ids). Everything else is proved: the
kids-or-fresh trichotomy classifies every occurrence by its realizer's
epoch, settled (kept, via anchor-liveness), in-flight (skipped), or beyond
(Lamport-fresh via `causal_mono` + `settledAt_dichotomy`). -/

theorem compactRanked_settled_reads {Γ : OrderedPrefixCode}
    {C : Configuration (E Γ α)} (hReach : EReach Γ C)
    (hGen : GenHonest (E Γ α) eApplicable C)
    (hEnum : CausalPastEnumerable (E Γ α) C)
    {v : Version} {s : EState α} {Ev S : Set (Op (EOp α))}
    (hv : C.ver v = some (s, Ev)) (hsettled : SettledAtOn C Ev S)
    (tree : List (List ℕ)) (live : List ℕ → Bool) (inflight : List (List ℕ))
    (htpos : ∀ k ∈ tree, PosChain k)
    (hTree : ∀ o, o ∈ C.events → eIsIns o = true → o ∈ S →
      ∃ k ∈ tree, coordOf Γ k = eCoord Γ o)
    (hTreeS : ∀ k ∈ tree, ∃ o, o ∈ S ∧ o ∈ C.events ∧ eIsIns o = true ∧
      coordOf Γ k = eCoord Γ o)
    (hLive : ∀ k ∈ tree, ∀ o, o ∈ C.events → o ∈ S → eIsIns o = true →
      coordOf Γ k = eCoord Γ o → (∀ dl ∈ S, dl.2.2 ≠ EOp.del o.1) →
      live k = true)
    (hInflight : ∀ o, o ∈ C.events → eIsIns o = true → o ∈ Ev → o ∉ S →
      ∃ q ∈ inflight, PosChain q ∧ coordOf Γ q = eCoord Γ o) :
    ∃ F : StablePrefixMap Γ,
      F.f = fStab Γ (rED (ePruneKeep tree live inflight) inflight)
        (ePruneKeep tree live inflight) ∧
      ∀ τ : List (Op (EOp α)), (∀ o ∈ τ, o ∈ C.events ∧ o ∉ Ev) →
        applySeq (E Γ α).toCRDTSig (eRemapSt F.f s) (τ.map (eRemapOp F.f))
            = eRemapSt F.f (applySeq (E Γ α).toCRDTSig s τ) ∧
          (E Γ α).query
              (applySeq (E Γ α).toCRDTSig (eRemapSt F.f s)
                (τ.map (eRemapOp F.f))) ()
            = (E Γ α).query (applySeq (E Γ α).toCRDTSig s τ) () := by
  classical
  obtain ⟨chainOf, hA⟩ := eAnchored_exists hGen hEnum
  have hHon : EHonest Γ C := eHonest_of_genHonest C hEnum hGen
  have hGood := e_goodConfig3 hReach
  have hEvSub : ∀ a ∈ Ev, a ∈ C.events :=
    fun a ha => hGood.ver_events_sub v s Ev hv a ha
  have hSsub : ∀ a ∈ S, a ∈ C.events := fun a ha => hEvSub a (hsettled.sub ha)
  have hirr : ∀ a : Op (EOp α), ¬ C.vis a a :=
    fun a ha => absurd (C.causal_mono ha) (Nat.lt_irrefl a.1)
  -- the chain of an event is pinned by its coordinate
  have hchain_eq : ∀ o, o ∈ C.events → eIsIns o = true → ∀ k, PosChain k →
      coordOf Γ k = eCoord Γ o → chainOf o.1 = k := by
    intro o ho hi k hk hck
    apply coordOf_inj Γ (hA.pos o ho hi) hk
    rw [← hA.coord o ho hi]
    exact hck.symm
  have hsum_node : ∀ a, a ∈ C.events → eIsIns a = true →
      ∀ p d, chainOf a.1 = p ++ [d] → a.1 = p.sum + d := by
    intro a ha hi p d hch
    have h1 := hA.sum a ha hi
    rw [hch] at h1
    simp only [List.sum_append, List.sum_cons, List.sum_nil,
      Nat.add_zero] at h1
    exact h1.symm
  have hids_eq : ∀ a b, a ∈ C.events → b ∈ C.events → eIsIns a = true →
      eIsIns b = true → chainOf a.1 = chainOf b.1 → a = b := by
    intro a b ha hb hai hbi hch
    apply (Configuration.core C).ts_unique ha hb
    have h1 := hA.sum a ha hai
    have h2 := hA.sum b hb hbi
    rw [hch] at h1
    exact h1.symm.trans h2
  set keep := ePruneKeep tree live inflight with hkeep
  -- the at-hand chain domain
  have hDpos : ∀ ch, EAtHand Γ C S Ev inflight chainOf ch → PosChain ch := by
    rintro ch ⟨o, ho, hi, rfl, -⟩
    exact hA.pos o ho hi
  have htree_of : ∀ a, a ∈ C.events → a ∈ S → eIsIns a = true →
      chainOf a.1 ∈ tree := by
    intro a haev haS hai
    obtain ⟨kt, hktm, hktc⟩ := hTree a haev hai haS
    rw [hchain_eq a haev hai kt (htpos kt hktm) hktc]
    exact hktm
  have hlive_of : ∀ a k, a ∈ C.events → a ∈ S → eIsIns a = true →
      chainOf a.1 = k → (∀ dl ∈ S, dl.2.2 ≠ EOp.del a.1) →
      k ∈ keep := by
    intro a k haev haS hai hak hnoSdel
    have hktree : k ∈ tree := hak ▸ htree_of a haev haS hai
    have hlv : live k = true := hLive k hktree a haev haS hai
      (by rw [← hak]; exact (hA.coord a haev hai).symm) hnoSdel
    exact mem_ePruneKeep.mpr ⟨hktree, Or.inl ⟨k, hktree, List.prefix_refl k, hlv⟩⟩
  -- the kept lemma: settled-realized nodes on at-hand chains survive pruning
  have hKept : ∀ (u ch : List ℕ), EAtHand Γ C S Ev inflight chainOf ch →
      ∀ k, ch = k ++ u → k ≠ [] →
      (∃ a, a ∈ C.events ∧ a ∈ S ∧ eIsIns a = true ∧ chainOf a.1 = k) →
      k ∈ keep := by
    intro u
    induction u with
    | nil =>
        rintro ch ⟨o, ho, hi, hcho, hcase⟩ k hch hkne ⟨a, haev, haS, hai, hak⟩
        rw [List.append_nil] at hch
        rw [hch] at hcho
        have hoa : o = a := hids_eq o a ho haev hi hai (by rw [hcho, hak])
        subst hoa
        rcases hcase with ⟨-, hcut⟩ | hinfl | hnotEv
        · exact hlive_of o k ho haS hi hak
            (fun dl hdl => hcut dl (hsettled.sub hdl))
        · rw [hak] at hinfl
          exact mem_ePruneKeep.mpr ⟨hak ▸ htree_of o ho haS hi,
            Or.inr ⟨k, hinfl, List.prefix_refl k⟩⟩
        · exact absurd (hsettled.sub haS) hnotEv
    | cons x u' ih =>
        rintro ch hD k hch hkne ⟨a, haev, haS, hai, hak⟩
        have hwit := hD
        obtain ⟨o, ho, hi, hcho, -⟩ := hwit
        have hpre : (k ++ [x]) <+: chainOf o.1 := by
          rw [hcho, hch]
          exact prefix_snoc_cons k x u'
        obtain ⟨b, hbev, hbi, hbk⟩ := hA.realize o ho hi k x hpre
        by_cases hbS : b ∈ S
        · have hk' : (k ++ [x]) ∈ keep := ih ch hD (k ++ [x])
            (by rw [hch]; simp) (by simp) ⟨b, hbev, hbS, hbi, hbk⟩
          exact ePruneKeep_prefix ⟨[x], rfl⟩ hk'
            (hak ▸ htree_of a haev haS hai)
        · by_cases hbEv : b ∈ Ev
          · obtain ⟨q, hqm, hqpos, hqc⟩ := hInflight b hbev hbi hbEv hbS
            have hqk : chainOf b.1 = q := hchain_eq b hbev hbi q hqpos hqc
            exact mem_ePruneKeep.mpr ⟨hak ▸ htree_of a haev haS hai,
              Or.inr ⟨q, hqm, by rw [← hqk, hbk]; exact ⟨[x], rfl⟩⟩⟩
          · -- b beyond the cut: its anchor is k's settled record, live in S
            obtain ⟨eb, πb, db, hop⟩ : ∃ eb πb db, b.2.2 = EOp.ins eb πb db := by
              obtain ⟨tb, rb, opb⟩ := b
              cases opb with
              | del y => simp [eIsIns] at hbi
              | ins eb πb db => exact ⟨eb, πb, db, rfl⟩
            obtain ⟨-, -, hchb⟩ := hA.anchored b hbev eb πb db hop
            have hcomb : k ++ [x] = chainOf db ++ [b.1 - db] :=
              hbk.symm.trans hchb
            have hdbk : chainOf db = k := by
              have h := congrArg List.dropLast hcomb
              rw [List.dropLast_concat, List.dropLast_concat] at h
              exact h.symm
            have hdb0 : db ≠ 0 := by
              intro h0
              rw [h0, hA.root] at hdbk
              exact hkne hdbk.symm
            obtain ⟨⟨a', ha'ev, ha'i, ha'1, -⟩, hblive⟩ :=
              hA.anchor_event b hbev eb πb db hop hdb0
            have ha'a : a' = a := hids_eq a' a ha'ev haev ha'i hai
              (by rw [ha'1, hdbk, hak])
            have hdba : db = a.1 := by rw [← ha'1, ha'a]
            refine hlive_of a k haev haS hai hak ?_
            intro dl hdl
            have hdlvis : C.vis dl b :=
              settledAt_dichotomy hsettled b hbev hbEv dl hdl
            have := hblive dl (hSsub dl hdl) hdlvis
            rwa [hdba] at this
  -- kids-or-fresh: the occurrence trichotomy
  have hocc : ∀ p d, Occ (EAtHand Γ C S Ev inflight chainOf) p d →
      skipAt inflight p = false →
      (p ++ [d]) ∈ keep ∨ ∀ e, (p ++ [e]) ∈ keep → e < d := by
    rintro p d ⟨ch, hD, hpre⟩ hskip
    have hwit := hD
    obtain ⟨o, ho, hi, hcho, -⟩ := hwit
    obtain ⟨b, hbev, hbi, hbk⟩ := hA.realize o ho hi p d
      (by rw [hcho]; exact hpre)
    by_cases hbS : b ∈ S
    · left
      obtain ⟨u, hu⟩ := hpre
      exact hKept u ch hD (p ++ [d]) hu.symm (by simp)
        ⟨b, hbev, hbS, hbi, hbk⟩
    · by_cases hbEv : b ∈ Ev
      · obtain ⟨q, hqm, hqpos, hqc⟩ := hInflight b hbev hbi hbEv hbS
        have : (p ++ [d]) ∈ inflight := by
          rw [← hbk, hchain_eq b hbev hbi q hqpos hqc]
          exact hqm
        exact absurd this (skipAt_eq_false.mp hskip d)
      · right
        intro e hke
        have hkt : (p ++ [e]) ∈ tree := ePruneKeep_subset _ hke
        obtain ⟨oe, hoeS, hoeev, hoei, hoec⟩ := hTreeS _ hkt
        have hoek : chainOf oe.1 = p ++ [e] :=
          hchain_eq oe hoeev hoei _ (htpos _ hkt) hoec
        have hlt := C.causal_mono
          (settledAt_dichotomy hsettled b hbev hbEv oe hoeS)
        rw [hsum_node oe hoeev hoei p e hoek,
          hsum_node b hbev hbi p d hbk] at hlt
        exact Nat.lt_of_add_lt_add_left hlt
  -- the bundle
  set F : StablePrefixMap Γ := compactRanked Γ tree live inflight
    (EAtHand Γ C S Ev inflight chainOf) htpos hDpos hocc with hFdef
  -- the canonical chain-aligned mints land in the bundle's MintAt
  have hMint : ∀ π δ, ChainMintBeyond Γ C S chainOf π δ →
      compactMintAt Γ keep (EAtHand Γ C S Ev inflight chainOf) π δ := by
    rintro π δ ⟨hδ, chA, hπ, hposA, o, ho, hi, hvisS, hcho⟩
    have hoS : o ∉ S := fun hoS => hirr o (hvisS o hoS)
    refine ⟨hδ, chA, hπ, hposA, ⟨o, ho, hi, hcho, ?_⟩, ?_⟩
    · by_cases hoEv : o ∈ Ev
      · obtain ⟨q, hqm, hqpos, hqc⟩ := hInflight o ho hi hoEv hoS
        exact Or.inr (Or.inl (by
          rw [hchain_eq o ho hi q hqpos hqc]; exact hqm))
      · exact Or.inr (Or.inr hoEv)
    · intro hk
      have hkt : (chA ++ [δ]) ∈ tree := ePruneKeep_subset _ hk
      obtain ⟨oe, hoeS, hoeev, hoei, hoec⟩ := hTreeS _ hkt
      have hoek : chainOf oe.1 = chA ++ [δ] :=
        hchain_eq oe hoeev hoei _ (htpos _ hkt) hoec
      have hooe : o = oe :=
        hids_eq o oe ho hoeev hi hoei (hcho.trans hoek.symm)
      exact hoS (hooe ▸ hoeS)
  have hAF : AnchorsFactorBeyond Γ F C S :=
    anchorsFactorBeyond_of_anchored hA F S hMint
  -- the cut state's coordinates are at rest (survival = never deleted in Ev)
  obtain ⟨ρ, hperm, hresp, happ⟩ := hGood.canonical v s Ev hv
  have hin : ∀ a ∈ Ev, a ∈ (Configuration.core C).events := by
    intro a ha
    rw [core_events]
    exact hEvSub a ha
  have hcl : ∀ a b, (Configuration.core C).vis a b →
      ¬ (E Γ α).toCRDTSig.commutes a b → b ∈ Ev → a ∈ Ev :=
    fun a b hvis _ hb => hGood.ver_causal v s Ev hv a b hvis hb
  have hwf := e_wf_of_enum (eHonest_core hHon) hin hcl hperm hresp
  have hrest : ∀ x ∈ s, F.Dom x.2.2 := by
    intro x hx
    rw [← happ] at hx
    obtain ⟨⟨o, hoρ, hoi, hrec⟩, hnd⟩ := (e_fold_mem Γ hwf x).mp hx
    have hoEv : o ∈ Ev := (hperm.2 o).mp hoρ
    have hoev : o ∈ C.events := hEvSub o hoEv
    have hx22 : x.2.2 = eCoord Γ o := by rw [hrec]; rfl
    have hx1 : x.1 = o.1 := by rw [hrec]; rfl
    refine Or.inl ⟨chainOf o.1, ⟨o, hoev, hoi, rfl, ?_⟩, by
      rw [hx22]; exact hA.coord o hoev hoi⟩
    by_cases hoS : o ∈ S
    · refine Or.inl ⟨hoS, fun dl hdl hddl => hnd ?_⟩
      rw [hx1]
      exact mem_eDels.mpr ⟨dl, (hperm.2 dl).mpr hdl, hddl⟩
    · obtain ⟨q, hqm, hqpos, hqc⟩ := hInflight o hoev hoi hoEv hoS
      exact Or.inr (Or.inl (by
        rw [hchain_eq o hoev hoi q hqpos hqc]; exact hqm))
  exact ⟨F, rfl, fun τ hτ =>
    eRecode_settled_bridge F hv hsettled hAF hrest τ hτ⟩

/-- **The composed headline, at the Elias-δ code**: at a `SettledAtOn`
cut of a disciplined honest configuration, the compaction, drop dead
ranges, rank-renumber in-flight-free sibling groups, re-encode with the
flipped Elias-δ code, preserves the fold and every read of every beyond-cut
continuation. Pure instantiation of `compactRanked_settled_reads`. -/
theorem compactEliasDelta_settled_reads
    {C : Configuration (E eliasDeltaCode α)}
    (hReach : EReach eliasDeltaCode C)
    (hGen : GenHonest (E eliasDeltaCode α) eApplicable C)
    (hEnum : CausalPastEnumerable (E eliasDeltaCode α) C)
    {v : Version} {s : EState α} {Ev S : Set (Op (EOp α))}
    (hv : C.ver v = some (s, Ev)) (hsettled : SettledAtOn C Ev S)
    (tree : List (List ℕ)) (live : List ℕ → Bool) (inflight : List (List ℕ))
    (htpos : ∀ k ∈ tree, PosChain k)
    (hTree : ∀ o, o ∈ C.events → eIsIns o = true → o ∈ S →
      ∃ k ∈ tree, coordOf eliasDeltaCode k = eCoord eliasDeltaCode o)
    (hTreeS : ∀ k ∈ tree, ∃ o, o ∈ S ∧ o ∈ C.events ∧ eIsIns o = true ∧
      coordOf eliasDeltaCode k = eCoord eliasDeltaCode o)
    (hLive : ∀ k ∈ tree, ∀ o, o ∈ C.events → o ∈ S → eIsIns o = true →
      coordOf eliasDeltaCode k = eCoord eliasDeltaCode o →
      (∀ dl ∈ S, dl.2.2 ≠ EOp.del o.1) → live k = true)
    (hInflight : ∀ o, o ∈ C.events → eIsIns o = true → o ∈ Ev → o ∉ S →
      ∃ q ∈ inflight, PosChain q ∧
        coordOf eliasDeltaCode q = eCoord eliasDeltaCode o) :
    ∃ F : StablePrefixMap eliasDeltaCode,
      F.f = fStab eliasDeltaCode
          (rED (ePruneKeep tree live inflight) inflight)
          (ePruneKeep tree live inflight) ∧
      ∀ τ : List (Op (EOp α)), (∀ o ∈ τ, o ∈ C.events ∧ o ∉ Ev) →
        applySeq (E eliasDeltaCode α).toCRDTSig
            (eRemapSt F.f s) (τ.map (eRemapOp F.f))
            = eRemapSt F.f (applySeq (E eliasDeltaCode α).toCRDTSig s τ) ∧
          (E eliasDeltaCode α).query
              (applySeq (E eliasDeltaCode α).toCRDTSig
                (eRemapSt F.f s) (τ.map (eRemapOp F.f))) ()
            = (E eliasDeltaCode α).query
                (applySeq (E eliasDeltaCode α).toCRDTSig s τ) () :=
  compactRanked_settled_reads hReach hGen hEnum hv hsettled tree live
    inflight htpos hTree hTreeS hLive hInflight

/-! ## §8 Axiom audit -/

#print axioms remapChain_keyLt
#print axioms rED_iso
#print axioms compactRanked_settled_reads
#print axioms compactEliasDelta_settled_reads

/-! ## §9 SPOT: the worked compaction, hand-derived (PASS + FAIL)

**PASS**: a delete-heavy epoch-0 history at the Elias-δ code (six inserts,
four deletes). Root group `{1,2,3,4,9}`, survivor `4`; `9` dead but kept (its
child `[9,5]` is live). `ePruneKeep` drops `[1],[2],[3]`; `rED` renumbers the
root group `4↦1, 9↦2` and the `[9]` group `5↦1`. Beyond the cut: a child of
the survivor (δ=6), a fresh root mint (δ=21, Lamport-fresh, dominating both
renumbered ordinals), and a delete. Reads pinned equal (`[108, 106, 107]`,
hand-derived: root deltas 21 > 9/2 dominate, ancestor before descendant);
coordinate weight pinned 40 → 24 bits (hand-summed: 13+18+9 vs 5+10+9).

**FAIL companion**: same cut, but an epoch-0 in-flight root insert (chain
`[6]`) is still undelivered. The *unguarded* dense renumbering (`rED` fed an
empty in-flight list, the tempting degenerate) maps `9↦2` under the
in-flight `6`, and the read flips to `[110, 106, 104]`: the late op jumps the
compacted survivor. The *guarded* construction (`skipAt` sees `[6]`) skips
the root group (`4,9` frozen), still renumbers the in-flight-free `[9]` group
(`5↦1`, 13→9 bits), and the read stays pinned `[106, 110, 104]`. -/

namespace CompactSPOT

open Sal.EmbedRGA (dEnc)

/-- Epoch 0, delete-heavy: chains `[1] [2] [3] [4] [9] [9,5]`; deletes kill
`1, 2, 3, 9`. Survivors: `104` (chain `[4]`), `106` (chain `[9,5]`). -/
def preOps : List (Op (EOp ℕ)) :=
  [ (1, 0, .ins 101 [] 0)
  , (2, 0, .ins 102 [] 0)
  , (3, 0, .ins 103 [] 0)
  , (4, 0, .ins 104 [] 0)
  , (9, 0, .ins 105 [] 0)
  , (14, 0, .ins 106 (dEnc 9) 9)
  , (15, 0, .del 1)
  , (16, 0, .del 2)
  , (17, 0, .del 3)
  , (18, 0, .del 9) ]

def sCut : EState ℕ := eFold eliasDeltaCode preOps

/-- The cut state, hand-derived: two survivors, the deep one carrying its
dead ancestor's 8-bit codeword. -/
theorem cut_state : sCut = [(14, 106, dEnc 9 ++ dEnc 5), (4, 104, dEnc 4)] := by
  native_decide

def tree0 : List (List ℕ) := [[1], [2], [3], [4], [9], [9, 5]]
def live0 : List ℕ → Bool := fun k => decide (k = [4] ∨ k = [9, 5])
def keep0 : List (List ℕ) := ePruneKeep tree0 live0 []

/-- **(a) DROP pinned**: the dead ranges `[1],[2],[3]` are dropped; dead `[9]`
is kept (live descendant). NOT the whole tree, NOT only the live leaves. -/
theorem keep_drops_dead : keep0 = [[4], [9], [9, 5]] ∧ keep0 ≠ tree0 := by
  native_decide

/-- The translation: rank-renumber + Elias-δ re-encode below `keep0`. -/
def gcf : List Bool → List Bool := fStab eliasDeltaCode (rED keep0 []) keep0

/-- **(b) RENUMBER pinned at codeword level**: `4 ↦ 1` (5 bits → 1),
`[9,5] ↦ [2,1]` (13 bits → 5). -/
theorem remap_concrete :
    gcf (dEnc 4) = dEnc 1 ∧ gcf (dEnc 9 ++ dEnc 5) = dEnc 2 ++ dEnc 1 := by
  native_decide

/-- Beyond the cut: a child of the deep survivor (δ = 6), a fresh root mint
(δ = 21), a delete of the shallow survivor. -/
def postOps : List (Op (EOp ℕ)) :=
  [ (20, 0, .ins 107 (dEnc 9 ++ dEnc 5) 14)
  , (21, 0, .ins 108 [] 0)
  , (22, 0, .del 4) ]

def finalO : EState ℕ := applySeq (E eliasDeltaCode).toCRDTSig sCut postOps

def finalR : EState ℕ :=
  applySeq (E eliasDeltaCode).toCRDTSig (eRemapSt gcf sCut)
    (postOps.map (eRemapOp gcf))

/-- PASS: compaction is invisible, both reads are the hand-derived
`[108, 106, 107]` (21 first, then the `9`-subtree, ancestor before child). -/
theorem reads_identical :
    SPOT.readE finalR = [108, 106, 107] ∧
    SPOT.readE finalO = [108, 106, 107] := by native_decide

/-- PASS: the compaction genuinely compresses under the Elias-δ code:
24 < 40 bits, hand-summed (`106`: 13→5, `107`: 18→10, `108`: 9→9). -/
theorem size_reduced :
    SPOT.coordWeight finalR = 24 ∧ SPOT.coordWeight finalO = 40 := by
  native_decide

/-- Degenerate-behavior pin: the read equality is NOT the identity map
echoing the state, the compacted state differs record-for-record. -/
theorem compaction_not_identity :
    eRemapSt gcf sCut ≠ sCut ∧ finalR ≠ finalO := by native_decide

/-! ### The FAIL companion: an in-flight sibling -/

/-- The in-flight epoch-0 op: a root insert (chain `[6]`), minted before the
cut, not yet delivered. -/
def flightOp : Op (EOp ℕ) := (6, 0, .ins 110 [] 0)

def inflight1 : List (List ℕ) := [[6]]

def keepF : List (List ℕ) := ePruneKeep tree0 live0 inflight1

/-- The guard, pinned: the root group has a known in-flight child ⟹ skipped;
the `[9]` group has none ⟹ renumbered. -/
theorem skip_guard :
    skipAt inflight1 [] = true ∧ skipAt inflight1 [9] = false := by
  native_decide

/-- Guarded map (skips the root group). -/
def gcfG : List Bool → List Bool :=
  fStab eliasDeltaCode (rED keepF inflight1) keepF

/-- UNGUARDED dense renumbering, the tempting degenerate: renumber every
kept group, ignoring the in-flight sibling. -/
def gcfU : List Bool → List Bool := fStab eliasDeltaCode (rED keepF []) keepF

def finalOF : EState ℕ := applySeq (E eliasDeltaCode).toCRDTSig sCut [flightOp]

def finalG : EState ℕ :=
  applySeq (E eliasDeltaCode).toCRDTSig (eRemapSt gcfG sCut)
    [eRemapOp gcfG flightOp]

def finalU : EState ℕ :=
  applySeq (E eliasDeltaCode).toCRDTSig (eRemapSt gcfU sCut)
    [eRemapOp gcfU flightOp]

/-- FAIL: unguarded dense renumbering FLIPS the pinned order, `9 ↦ 2` slides
the compacted survivor under the in-flight `6`, and the late op jumps from
the middle to the front. -/
theorem unguarded_flips_order :
    SPOT.readE finalOF = [106, 110, 104] ∧
    SPOT.readE finalU = [110, 106, 104] ∧
    SPOT.readE finalU ≠ SPOT.readE finalOF := by native_decide

/-- PASS: the guarded construction skips exactly that group and the read
stays pinned, while the in-flight-free `[9]` group still compresses
(23 → 19 bits: `106` sheds 4 bits of dead-delta codeword). -/
theorem guarded_skips_group :
    SPOT.readE finalG = [106, 110, 104] ∧
    SPOT.coordWeight finalG = 19 ∧ SPOT.coordWeight finalOF = 23 := by
  native_decide

#print axioms cut_state
#print axioms keep_drops_dead
#print axioms remap_concrete
#print axioms reads_identical
#print axioms size_reduced
#print axioms compaction_not_identity
#print axioms skip_guard
#print axioms unguarded_flips_order
#print axioms guarded_skips_group

end CompactSPOT

end Sal.ConditionedMRDTs
