Forward bound (brick 3b): T P is level-canonical, for every degree d.

The crux geometric half of the Reconstruction Lemma: the delete-min survivors T P of a critical portrait are always level-canonical, ∀ j < d, #{u ∈ T P : level u ≤ j} ≤ j. This is the global non-crossing/ballot "Catalan heart" of the general census proof, here proved for ALL d (sorry-free, native_decide-free; axioms ⊆ {propext, Classical.choice, Quot.sound}). Follows the paper proof docs/b2_forward_reconstruction_2026-06-16.md (Lemma A laminar, Lemma B monotone columns, the Kernel, the laminar-forest recursion); probe probes/check_b2_forward.py confirms d ≤ 6.

The proof has two parts.

• PART I (AbstractLaminar) — a self-contained combinatorial result about a finite family of half-open integer intervals (lo e, hi e] with columns col e, pairwise laminar (Lemma A), interval-injective, with the Lemma-B column monotonicities (bRight/bLeft/bSeam). The master bound N(a,b) ≤ b - a packages the Kernel (g(e) ≤ h(e) - 1), the laminar-forest recursion, and the no-tiling crux (a column scan c* < q₁ ≤ ⋯ ≤ qₖ < c*).

• PART II (CriticalPortraits) — the geometric edge model. Edges ARE the survivors: each survivor x ∈ T P is the top of a unique edge whose other endpoint is its immediate predecessor predIn x in its host critical set. hi x = level x, col x = fiber x, lo x = level (predIn x). Lemmas A/B + interval-injectivity all reduce to ONE master non-alternation lemma no_alt (no two survivors' endpoints alternate px < py < x < y), which dispatches cross-host via the portrait's Unlinked clause and same-host via predecessor immediacy. Assembling the Family and applying the master bound at window (0, j] gives T_levelCanonical.

PART I — Abstract laminar interval family: Kernel + forest recursion.

A finite family E : Finset ι of half-open integer intervals (lo e, hi e] with columns col e, pairwise laminar (Lemma A), intervals identifying edges (inj), and the Lemma-B column properties (bRight/bLeft/bSeam). The master bound N(a,b) := #{e ∈ E : a ≤ lo e ∧ hi e ≤ b} ≤ b - a packages the Kernel + the laminar-forest recursion + the no-tiling crux.

structure AbstractLaminar.Family (ι : Type u_2) [DecidableEq ι] : Type u_2

An abstract laminar family: an index set with low/high endpoints and a column.

• E : Finset ι

  The carrier index set of the family.

• lo : ι → ℕ

  The low endpoint of each index.

• hi : ι → ℕ

  The high endpoint of each index.

• col : ι → ℕ

  The column of each index.

• lh (e : ι) : e ∈ self.E → self.lo e < self.hi e
• inj (e : ι) : e ∈ self.E → ∀ f ∈ self.E, self.lo e = self.lo f → self.hi e = self.hi f → e = f
• laminar (e : ι) : e ∈ self.E → ∀ f ∈ self.E, ¬(self.lo e < self.lo f ∧ self.lo f < self.hi e ∧ self.hi e < self.hi f)
• bRight (e : ι) : e ∈ self.E → ∀ f ∈ self.E, self.hi e = self.hi f → self.lo e < self.lo f → self.col f < self.col e
• bLeft (e : ι) : e ∈ self.E → ∀ f ∈ self.E, self.lo e = self.lo f → self.hi f < self.hi e → self.col e < self.col f
• bSeam (e : ι) : e ∈ self.E → ∀ f ∈ self.E, self.hi e = self.lo f → self.col e ≤ self.col f

def AbstractLaminar.contained {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) : Finset ι

Edges contained in the window (a, b].

Equations

• AbstractLaminar.contained fam a b = {e ∈ fam.E | a ≤ fam.lo e ∧ fam.hi e ≤ b}

def AbstractLaminar.N {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) : ℕ

The count N(a,b).

Equations

• AbstractLaminar.N fam a b = (AbstractLaminar.contained fam a b).card

theorem AbstractLaminar.mem_contained {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {e : ι} : e ∈ contained fam a b ↔ e ∈ fam.E ∧ a ≤ fam.lo e ∧ fam.hi e ≤ b

theorem AbstractLaminar.N_eq_zero_of_le {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} (hba : b ≤ a) : N fam a b = 0

Empty window: no contained edges.

theorem AbstractLaminar.overlap_imp_nested {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {e f : ι} (he : e ∈ fam.E) (hf : f ∈ fam.E) (h1 : fam.lo e < fam.hi f) (h2 : fam.lo f < fam.hi e) : fam.lo f ≤ fam.lo e ∧ fam.hi e ≤ fam.hi f ∨ fam.lo e ≤ fam.lo f ∧ fam.hi f ≤ fam.hi e

Two overlapping edges are nested (laminarity).

def AbstractLaminar.IsStrict {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) (e : ι) : Prop

"strict": interval not exactly the window.

Equations

• AbstractLaminar.IsStrict fam a b e = (fam.lo e ≠ a ∨ fam.hi e ≠ b)

@[implicit_reducible]

instance AbstractLaminar.instDecidableIsStrict {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) (e : ι) : Decidable (IsStrict fam a b e)

Equations

• AbstractLaminar.instDecidableIsStrict fam a b e = id inferInstance

def AbstractLaminar.Sstrict {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) : Finset ι

The strictly-contained indices of fam on the window [a, b].

Equations

• AbstractLaminar.Sstrict fam a b = Finset.filter (AbstractLaminar.IsStrict fam a b) (AbstractLaminar.contained fam a b)

theorem AbstractLaminar.mem_Sstrict {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {e : ι} : e ∈ Sstrict fam a b ↔ (e ∈ fam.E ∧ a ≤ fam.lo e ∧ fam.hi e ≤ b) ∧ (fam.lo e ≠ a ∨ fam.hi e ≠ b)

def AbstractLaminar.containersS {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) (f : ι) : Finset ι

Strict edges containing f.

Equations

• AbstractLaminar.containersS fam a b f = {g ∈ AbstractLaminar.Sstrict fam a b | fam.lo g ≤ fam.lo f ∧ fam.hi f ≤ fam.hi g}

theorem AbstractLaminar.mem_containersS {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f g : ι} : g ∈ containersS fam a b f ↔ ((g ∈ fam.E ∧ a ≤ fam.lo g ∧ fam.hi g ≤ b) ∧ (fam.lo g ≠ a ∨ fam.hi g ≠ b)) ∧ fam.lo g ≤ fam.lo f ∧ fam.hi f ≤ fam.hi g

theorem AbstractLaminar.containersS_nonempty {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : (containersS fam a b f).Nonempty

noncomputable def AbstractLaminar.rootS {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) (f : ι) : ι

The strict root of f: widest strict containing edge (total; junk = f off Sstrict).

Equations

• AbstractLaminar.rootS fam a b f = if hf : f ∈ AbstractLaminar.Sstrict fam a b then ⋯.choose else f

theorem AbstractLaminar.rootS_mem_containersS {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : rootS fam a b f ∈ containersS fam a b f

theorem AbstractLaminar.rootS_max {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) (g : ι) : g ∈ containersS fam a b f → fam.hi g - fam.lo g ≤ fam.hi (rootS fam a b f) - fam.lo (rootS fam a b f)

theorem AbstractLaminar.rootS_mem_E {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : rootS fam a b f ∈ fam.E

theorem AbstractLaminar.rootS_mem_Sstrict {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : rootS fam a b f ∈ Sstrict fam a b

theorem AbstractLaminar.rootS_window {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : a ≤ fam.lo (rootS fam a b f) ∧ fam.hi (rootS fam a b f) ≤ b

theorem AbstractLaminar.rootS_strict {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : fam.lo (rootS fam a b f) ≠ a ∨ fam.hi (rootS fam a b f) ≠ b

theorem AbstractLaminar.rootS_contains {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : fam.lo (rootS fam a b f) ≤ fam.lo f ∧ fam.hi f ≤ fam.hi (rootS fam a b f)

theorem AbstractLaminar.rootS_width_lt {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : fam.hi (rootS fam a b f) - fam.lo (rootS fam a b f) < b - a

The root's width is strictly less than the window's width.

theorem AbstractLaminar.rootS_maximal {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) {g : ι} (hg : g ∈ Sstrict fam a b) (h1 : fam.lo g ≤ fam.lo (rootS fam a b f)) (h2 : fam.hi (rootS fam a b f) ≤ fam.hi g) : fam.lo g = fam.lo (rootS fam a b f) ∧ fam.hi g = fam.hi (rootS fam a b f)

The root is maximal among strict edges.

theorem AbstractLaminar.rootS_idem {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : rootS fam a b (rootS fam a b f) = rootS fam a b f

Root is idempotent.

noncomputable def AbstractLaminar.Roots {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) : Finset ι

The roots in window (a,b]: maximal strict edges.

Equations

• AbstractLaminar.Roots fam a b = {r ∈ AbstractLaminar.Sstrict fam a b | AbstractLaminar.rootS fam a b r = r}

theorem AbstractLaminar.mem_Roots {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {r : ι} : r ∈ Roots fam a b ↔ r ∈ Sstrict fam a b ∧ rootS fam a b r = r

theorem AbstractLaminar.rootS_mem_Roots {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {f : ι} (hf : f ∈ Sstrict fam a b) : rootS fam a b f ∈ Roots fam a b

theorem AbstractLaminar.root_self_props {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {r : ι} (hr : r ∈ Roots fam a b) : r ∈ fam.E ∧ a ≤ fam.lo r ∧ fam.hi r ≤ b ∧ (fam.lo r ≠ a ∨ fam.hi r ≠ b)

theorem AbstractLaminar.root_unique {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {r r' : ι} (hr : r ∈ Roots fam a b) (hr' : r' ∈ Roots fam a b) {g : ι} (hg : g ∈ fam.E) (h1 : fam.lo r ≤ fam.lo g) (h2 : fam.hi g ≤ fam.hi r) (h1' : fam.lo r' ≤ fam.lo g) (h2' : fam.hi g ≤ fam.hi r') : r = r'

Uniqueness: two roots that both contain g's interval coincide.

theorem AbstractLaminar.fiber_eq_contained {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {r : ι} (hr : r ∈ Roots fam a b) : {g ∈ Sstrict fam a b | rootS fam a b g = r} = contained fam (fam.lo r) (fam.hi r)

The fiber of a root r equals the subtree contained (lo r) (hi r).

theorem AbstractLaminar.Sstrict_card_eq_sum {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} : (Sstrict fam a b).card = ∑ r ∈ Roots fam a b, N fam (fam.lo r) (fam.hi r)

Strict edges decompose as the sum of root subtrees.

def AbstractLaminar.topEdges {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) : Finset ι

Edges with interval exactly the window.

Equations

• AbstractLaminar.topEdges fam a b = {e ∈ AbstractLaminar.contained fam a b | fam.lo e = a ∧ fam.hi e = b}

theorem AbstractLaminar.topEdges_card_le {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} : (topEdges fam a b).card ≤ 1

At most one top edge (intervals identify edges).

theorem AbstractLaminar.Sstrict_eq_filter_not {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} : Sstrict fam a b = {e ∈ contained fam a b | ¬(fam.lo e = a ∧ fam.hi e = b)}

Sstrict is the complementary filter to topEdges.

theorem AbstractLaminar.N_split {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} : N fam a b = (topEdges fam a b).card + (Sstrict fam a b).card

N = #topEdges + #Sstrict.

theorem AbstractLaminar.roots_interval_disjoint {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {r r' : ι} (hr : r ∈ Roots fam a b) (hr' : r' ∈ Roots fam a b) (hne : r ≠ r') : fam.hi r ≤ fam.lo r' ∨ fam.hi r' ≤ fam.lo r

Distinct roots have disjoint half-open level-intervals.

theorem AbstractLaminar.roots_Ioc_disjoint {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} : (↑(Roots fam a b)).PairwiseDisjoint fun (r : ι) => Finset.Ioc (fam.lo r) (fam.hi r)

The Finset.Ioc intervals of distinct roots are disjoint.

theorem AbstractLaminar.roots_width_sum_le {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} : ∑ r ∈ Roots fam a b, (fam.hi r - fam.lo r) ≤ b - a

Sum of root widths is at most the window width.

theorem AbstractLaminar.crux {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} (hab : a < b) (htop : (topEdges fam a b).Nonempty) : ∑ r ∈ Roots fam a b, (fam.hi r - fam.lo r) ≤ b - a - 1

THE CRUX: if the window has a top edge, the root subtree widths do not cover it.

theorem AbstractLaminar.master {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (a b : ℕ) : N fam a b ≤ b - a

The master counting bound N(a,b) ≤ b - a.

PART II — The geometric edge model (edges = survivors) and the forward bound.

Phase -1: arithmetic engine reused everywhere.

theorem CriticalPortraits.val_decomp {N m : ℕ} (i : ZMod N) : i.val = i.val % m + i.val / m * m

i.val = (i.val % m) + (i.val / m) * m.

theorem CriticalPortraits.sameblock_lt {N m : ℕ} (hm : 0 < m) {x y : ZMod N} (ha : x.val / m < y.val / m) : x.val < y.val

ENGINE: a single level of separation beats any column offset, ANY fibers.

theorem CriticalPortraits.critical_sameFiber {d m : ℕ} {S : Finset (ZMod (d * m))} (hS : IsCriticalSet d m S) {x y : ZMod (d * m)} (hx : x ∈ S) (hy : y ∈ S) : x.val % m = y.val % m

Members of a critical set share a fiber (column).

Phase 0a: host-set recovery (the edge's home critical set).

noncomputable def CriticalPortraits.hostSet {d m : ℕ} (P : Finset (Finset (ZMod (d * m)))) (x : ZMod (d * m)) (hx : x ∈ T P) : Finset (ZMod (d * m))

The host critical set of an edge x in T P.

Equations

• CriticalPortraits.hostSet P x hx = ⋯.choose

theorem CriticalPortraits.hostSet_mem {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) : hostSet P x hx ∈ P

theorem CriticalPortraits.mem_eraseMin_hostSet {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) : x ∈ eraseMin (hostSet P x hx)

theorem CriticalPortraits.mem_hostSet {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) : x ∈ hostSet P x hx

Phase 0b: predecessor = the other endpoint (immediate predecessor in the host).

def CriticalPortraits.belowIn {d m : ℕ} (S : Finset (ZMod (d * m))) (x : ZMod (d * m)) : Finset (ZMod (d * m))

The elements of S strictly below x in value.

Equations

• CriticalPortraits.belowIn S x = {y ∈ S | y.val < x.val}

theorem CriticalPortraits.belowIn_nonempty {d m : ℕ} [NeZero (d * m)] {S : Finset (ZMod (d * m))} (h : S.Nonempty) {x : ZMod (d * m)} (hx : x ∈ eraseMin S) : (belowIn S x).Nonempty

noncomputable def CriticalPortraits.predIn {d m : ℕ} [NeZero (d * m)] (P : Finset (Finset (ZMod (d * m)))) (x : ZMod (d * m)) (hx : x ∈ T P) : ZMod (d * m)

The immediate predecessor of survivor x inside its host set: the .val-greatest element of the host strictly below x.

Equations

• CriticalPortraits.predIn P x hx = ⋯.choose

theorem CriticalPortraits.predIn_mem_belowIn {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) : predIn P x hx ∈ belowIn (hostSet P x hx) x

theorem CriticalPortraits.predIn_max {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) (y : ZMod (d * m)) : y ∈ belowIn (hostSet P x hx) x → y.val ≤ (predIn P x hx).val

theorem CriticalPortraits.predIn_mem_host {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) : predIn P x hx ∈ hostSet P x hx

theorem CriticalPortraits.predIn_val_lt {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) : (predIn P x hx).val < x.val

theorem CriticalPortraits.hostSet_critical {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x : ZMod (d * m)} (hx : x ∈ T P) : IsCriticalSet d m (hostSet P x hx)

The host set of a survivor is critical.

theorem CriticalPortraits.predIn_sameFiber {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x : ZMod (d * m)} (hx : x ∈ T P) : (predIn P x hx).val % m = x.val % m

Predecessor shares the survivor's fiber.

theorem CriticalPortraits.predIn_level_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x : ZMod (d * m)} (hx : x ∈ T P) : (predIn P x hx).val / m < x.val / m

The edge is nonempty: lo < hi in level.

theorem CriticalPortraits.predIn_immediate {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) {z : ZMod (d * m)} (hz : z ∈ hostSet P x hx) (h1 : (predIn P x hx).val < z.val) (h2 : z.val < x.val) : False

predIn x is the immediate predecessor: no host element strictly between it and x.

Phase 1: the crossing engine.

theorem CriticalPortraits.cross_false {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x y : ZMod (d * m)} (hx : x ∈ T P) (hy : y ∈ T P) (hhost : hostSet P x hx ≠ hostSet P y hy) (o1 : (predIn P x hx).val < (predIn P y hy).val) (o2 : (predIn P y hy).val < x.val) (o3 : x.val < y.val) : False

Cross-host crossing: an alternating val-quadruple px < py < x < y with px,x in host x and py,y in host y (distinct hosts) contradicts the portrait's Unlinked clause.

Phase 2: total edge data (loV, hiV, colV).

def CriticalPortraits.hiV {d m : ℕ} (x : ZMod (d * m)) : ℕ

The level index x.val / m of a position x.

Equations

• CriticalPortraits.hiV x = x.val / m

def CriticalPortraits.colV {d m : ℕ} (x : ZMod (d * m)) : ℕ

The fiber index x.val % m of a position x.

Equations

• CriticalPortraits.colV x = x.val % m

noncomputable def CriticalPortraits.loV {d m : ℕ} [NeZero (d * m)] (P : Finset (Finset (ZMod (d * m)))) (x : ZMod (d * m)) : ℕ

The low interval-endpoint value of x within its host critical set.

Equations

• CriticalPortraits.loV P x = if hx : x ∈ CriticalPortraits.T P then (CriticalPortraits.predIn P x hx).val / m else 0

theorem CriticalPortraits.loV_eq {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {x : ZMod (d * m)} (hx : x ∈ T P) : loV P x = (predIn P x hx).val / m

theorem CriticalPortraits.top_val_eq {d m : ℕ} {x : ZMod (d * m)} : x.val = colV x + hiV x * m

The survivor's value decomposes as colV + hiV*m.

theorem CriticalPortraits.pred_val_eq {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x : ZMod (d * m)} (hx : x ∈ T P) : (predIn P x hx).val = colV x + loV P x * m

The predecessor's value decomposes as colV + loV*m (same column as the survivor).

Phase 3: the master non-alternation + same-host glue.

theorem CriticalPortraits.no_alt {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x y : ZMod (d * m)} (hx : x ∈ T P) (hy : y ∈ T P) (o1 : (predIn P x hx).val < (predIn P y hy).val) (o2 : (predIn P y hy).val < x.val) (o3 : x.val < y.val) : False

THE MASTER NON-ALTERNATION LEMMA. No two survivors' endpoints alternate as px < py < x < y (covers cross-host via Unlinked and same-host via immediacy).

theorem CriticalPortraits.eq_imp_sameHost {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x y : ZMod (d * m)} (hx : x ∈ T P) (hy : y ∈ T P) (hxy : x = y) : hostSet P x hx = hostSet P y hy

If two survivors coincide as points they share a host (Portrait disjointness).

theorem CriticalPortraits.predEq_imp_sameHost {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x y : ZMod (d * m)} (hx : x ∈ T P) (hy : y ∈ T P) [NeZero (d * m)] (hpe : predIn P x hx = predIn P y hy) : hostSet P x hx = hostSet P y hy

If predecessors coincide as points the survivors share a host.

Phase 4: the LEMMA A / LEMMA B / inj axioms (in loV/hiV/colV).

theorem CriticalPortraits.colV_lt_m {d m : ℕ} (hm : 0 < m) (x : ZMod (d * m)) : colV x < m

theorem CriticalPortraits.lemmaA {d m : ℕ} [NeZero (d * m)] (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e f : ZMod (d * m)} (he : e ∈ T P) (hf : f ∈ T P) (h1 : loV P e < loV P f) (h2 : loV P f < hiV e) (h3 : hiV e < hiV f) : False

LEMMA A: laminar (no proper overlap of level-intervals).

theorem CriticalPortraits.lemmaB_seam {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e f : ZMod (d * m)} (he : e ∈ T P) (hf : f ∈ T P) (hseam : hiV e = loV P f) : colV e ≤ colV f

LEMMA B (seam): e tops where f bottoms ⇒ col e ≤ col f.

theorem CriticalPortraits.lemmaB_right {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e f : ZMod (d * m)} (he : e ∈ T P) (hf : f ∈ T P) (htop : hiV e = hiV f) (hlo : loV P e < loV P f) : colV f < colV e

LEMMA B (right-aligned): share top, nested right ⇒ inner col smaller.

theorem CriticalPortraits.lemmaB_left {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e f : ZMod (d * m)} (he : e ∈ T P) (hf : f ∈ T P) (hbot : loV P e = loV P f) (hhi : hiV f < hiV e) : colV e < colV f

LEMMA B (left-aligned): share bottom, nested left ⇒ inner col larger.

theorem CriticalPortraits.edge_inj {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e f : ZMod (d * m)} (he : e ∈ T P) (hf : f ∈ T P) (hlo : loV P e = loV P f) (hhi : hiV e = hiV f) : e = f

INJECTIVITY: distinct survivors have distinct level-intervals.

Phase 5: the Family instance and the forward bound.

noncomputable def CriticalPortraits.survivorFamily {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) : AbstractLaminar.Family (ZMod (d * m))

The laminar interval family of a portrait's survivors (edges = survivors).

Equations

• One or more equations did not get rendered due to their size.

theorem CriticalPortraits.T_levelCanonical {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) : LevelCanonical d m (T P)

FORWARD BOUND. T P is level-canonical, for every degree d.