Surjectivity of T via the balance forest β (Part II of the bijection).

For a level-canonical (d-1)-subset U ⊆ ZMod (d*m), the balance forest β(U) is the explicit critical portrait with T(β(U)) = U — the discriminating section property (a wrong parent rule fails this). Construction (paper Part II / bare-Lean betaParent):

• For a survivor u (fiber φ = u.val % m, level lu = u.val / m) and level k, the deficiency is D(k) = S(φ+k·m, u) − (lu−k−1) where S(x,y) = #{t∈U : x<t.val<y} (Scount).
• betaK U u is the largest k ≤ lu−1 with D(k)=0 (Nat.findGreatest); betaParent U u is the fiber-φ point at level betaK.
• β(U) (beta) is the set of connected components (betaBlock) of the parent edges (v*(u),u), recovered via Relation.ReflTransGen of the adjacency relation bAdj. Each block's minVal is its non-U root (betaRoot); the survivors of each block are exactly its U-points.

PROVED (sorry-free, axioms ⊆ {propext, Classical.choice, Quot.sound}):

• discrete_ivt — discrete IVT via Nat.findGreatest; exists_balance (E) + betaK_max (M2).
• Defc_pos_after — M2 strict positivity (the prefix/GPRE bound): the deficiency is > 0 strictly past the balance index (a second use of the discrete IVT, on [j, lu-1]).
• betaParent_inj (I, parent injectivity, via the deficiency additive split + maximality).
• T_beta — T(β(U)) = U (the load-bearing, discriminating spec).
• betaBlock_critical (IsCriticalSet per block), beta_pairwise_disjoint, beta_weight (∑(|S|−1)=d−1) — three of the four Portrait conjuncts.
• beta_unlinked (N) is REDUCED to beta_interval_closed and PROVED from it.

NOW FULLY PROVED (no remaining sorry):

• beta_interval_closed — the geometric heart of N: a point of one block strictly inside another block's .val-span forces the whole block inside. Proved via the no-escape property P (noEscape, a second discrete IVT on ψ-points anchored by the Q deficiency bound, with the GPRE prefix bound and N0 window lemma; the ψ ≥ φ / ψ < φ fiber split is handled by sep_master), then the laminarity bridge (root_ge, descend_cross) turns P into the two-sided .val-span containment using betaBlock_disjoint. Downstream (beta_unlinked, beta_portrait, T_surjOn) is therefore complete: SURJECTIVITY of T (all d) is proved. Axioms: {propext, Classical.choice, Quot.sound} (no sorryAx, no native_decide).

Layer 0: discrete IVT via Nat.findGreatest.

theorem CriticalPortraits.discrete_ivt (D : ℕ → ℤ) (L : ℕ) (h0 : D 0 ≤ 0) (hL : 0 ≤ D L) (hstep : ∀ k < L, D (k + 1) ≤ D k + 1) : ∃ k ≤ L, D k = 0

Discrete IVT. An integer-valued sequence with D 0 ≤ 0, 0 ≤ D L, and unit-bounded up-steps (D (k+1) ≤ D k + 1) hits zero somewhere in [0, L].

Layer 1: Scount and the deficiency.

def CriticalPortraits.Scount {d m : ℕ} (U : Finset (ZMod (d * m))) (x y : ℕ) : ℕ

S(x,y) = #{t ∈ U : x < t.val < y}.

Equations

• CriticalPortraits.Scount U x y = {t ∈ U | x < t.val ∧ t.val < y}.card

theorem CriticalPortraits.Scount_antitone_left {d m : ℕ} (U : Finset (ZMod (d * m))) {x x' y : ℕ} (hxx : x ≤ x') : Scount U x' y ≤ Scount U x y

Enlarging the lower endpoint shrinks the open interval: Scount is antitone in x.

def CriticalPortraits.Defc {d m : ℕ} (U : Finset (ZMod (d * m))) (φ lu uval k : ℕ) : ℤ

The integer deficiency of survivor u (column φ, level lu) at index k: D(k) = Scount U (φ + k*m) u.val − (lu − k − 1).

Equations

• CriticalPortraits.Defc U φ lu uval k = ↑(CriticalPortraits.Scount U (φ + k * m) uval) - (↑lu - ↑k - 1)

theorem CriticalPortraits.Defc_step {d m : ℕ} (_hm : 0 < m) (U : Finset (ZMod (d * m))) (φ lu uval k : ℕ) : Defc U φ lu uval (k + 1) ≤ Defc U φ lu uval k + 1

The deficiency has unit-bounded up-steps (the E3 step bound).

theorem CriticalPortraits.Defc_top_nonneg {d m : ℕ} (U : Finset (ZMod (d * m))) (φ lu uval : ℕ) (hlu : 1 ≤ lu) : 0 ≤ Defc U φ lu uval (lu - 1)

E1 (upper boundary). D(lu-1) ≥ 0: the constant (lu - (lu-1) - 1) = 0 and Scount ≥ 0.

theorem CriticalPortraits.Scount_bot_le {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) : Scount U (u.val % m) u.val ≤ u.val / m - 1

The scount bound from canonicity: #{t ∈ U : φ < t.val < u.val} ≤ lu - 1.

theorem CriticalPortraits.Defc_bot_nonpos {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) (hlu : 1 ≤ u.val / m) : Defc U (u.val % m) (u.val / m) u.val 0 ≤ 0

E2 (lower boundary). D(0) ≤ 0 from canonicity.

Layer 2: existence of a balance index.

theorem CriticalPortraits.exists_balance {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) (hlu : 1 ≤ u.val / m) : ∃ k ≤ u.val / m - 1, Defc U (u.val % m) (u.val / m) u.val k = 0

Existence (E). For a survivor u of a canonical U with level ≥ 1, some balance index k ≤ lu-1 has deficiency 0.

theorem CriticalPortraits.level_lt_d {d m : ℕ} (_hm : 0 < m) (x : ZMod (d * m)) [NeZero (d * m)] : x.val / m < d

Every position has level < d.

Layer 3: the balance index betaK, parent value and parent point.

noncomputable def CriticalPortraits.betaK {d m : ℕ} (U : Finset (ZMod (d * m))) (u : ZMod (d * m)) : ℕ

The largest balance index K of survivor u (the highest balance parent's level).

Equations

• CriticalPortraits.betaK U u = Nat.findGreatest (fun (k : ℕ) => CriticalPortraits.Defc U (u.val % m) (u.val / m) u.val k = 0) (u.val / m - 1)

theorem CriticalPortraits.betaK_le {d m : ℕ} (U : Finset (ZMod (d * m))) (u : ZMod (d * m)) : betaK U u ≤ u.val / m - 1

betaK ≤ lu - 1.

theorem CriticalPortraits.betaK_spec {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) (hlu : 1 ≤ u.val / m) : Defc U (u.val % m) (u.val / m) u.val (betaK U u) = 0

betaK is a balance index: deficiency 0 there.

theorem CriticalPortraits.betaK_max {d m : ℕ} {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} {j : ℕ} (hj1 : betaK U u < j) (hj2 : j ≤ u.val / m - 1) : Defc U (u.val % m) (u.val / m) u.val j ≠ 0

Maximality (M2). For betaK < j ≤ lu-1, deficiency at j is nonzero.

noncomputable def CriticalPortraits.betaParentVal {d m : ℕ} (U : Finset (ZMod (d * m))) (u : ZMod (d * m)) : ℕ

The parent value: φ + betaK*m (same fiber as u, level betaK).

Equations

• CriticalPortraits.betaParentVal U u = u.val % m + CriticalPortraits.betaK U u * m

theorem CriticalPortraits.betaParentVal_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} (hlu : 1 ≤ u.val / m) : betaParentVal U u < d * m

The parent value is < d*m (so its ZMod point round-trips).

noncomputable def CriticalPortraits.betaParent {d m : ℕ} (U : Finset (ZMod (d * m))) (u : ZMod (d * m)) : ZMod (d * m)

The parent point: the ZMod element at betaParentVal.

Equations

• CriticalPortraits.betaParent U u = ↑(CriticalPortraits.betaParentVal U u)

theorem CriticalPortraits.betaParent_val {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} (hlu : 1 ≤ u.val / m) : (betaParent U u).val = betaParentVal U u

betaParent's .val is exactly betaParentVal (round-trips since it is < d*m).

theorem CriticalPortraits.betaParent_fiber {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} (hlu : 1 ≤ u.val / m) : (betaParent U u).val % m = u.val % m

betaParent shares u's fiber.

theorem CriticalPortraits.betaParent_level {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} (hlu : 1 ≤ u.val / m) : (betaParent U u).val / m = betaK U u

betaParent's level is betaK (strictly below u's level).

theorem CriticalPortraits.betaParent_level_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} (hlu : 1 ≤ u.val / m) : (betaParent U u).val / m < u.val / m

betaParent's level is strictly below u's level.

theorem CriticalPortraits.betaParent_val_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} (hlu : 1 ≤ u.val / m) : (betaParent U u).val < u.val

betaParent's .val is strictly below u's .val.

Layer 4: adjacency, reachability, and blocks as components.

def CriticalPortraits.bEdge {d m : ℕ} (U : Finset (ZMod (d * m))) (a b : ZMod (d * m)) : Prop

The (directed) parent step: b is a survivor (level ≥ 1) and a is its balance parent.

Equations

• CriticalPortraits.bEdge U a b = (b ∈ U ∧ 1 ≤ b.val / m ∧ a = CriticalPortraits.betaParent U b)

def CriticalPortraits.bAdj {d m : ℕ} (U : Finset (ZMod (d * m))) (a b : ZMod (d * m)) : Prop

The adjacency relation (symmetrized parent step).

Equations

• CriticalPortraits.bAdj U a b = (CriticalPortraits.bEdge U a b ∨ CriticalPortraits.bEdge U b a)

theorem CriticalPortraits.bAdj_symm {d m : ℕ} {U : Finset (ZMod (d * m))} {a b : ZMod (d * m)} (h : bAdj U a b) : bAdj U b a

def CriticalPortraits.bReach {d m : ℕ} (U : Finset (ZMod (d * m))) (a b : ZMod (d * m)) : Prop

Reachability: the reflexive-transitive closure of adjacency.

Equations

• CriticalPortraits.bReach U a b = Relation.ReflTransGen (CriticalPortraits.bAdj U) a b

theorem CriticalPortraits.bReach_refl {d m : ℕ} {U : Finset (ZMod (d * m))} (a : ZMod (d * m)) : bReach U a a

theorem CriticalPortraits.bReach_symm {d m : ℕ} {U : Finset (ZMod (d * m))} {a b : ZMod (d * m)} (h : bReach U a b) : bReach U b a

theorem CriticalPortraits.bReach_trans {d m : ℕ} {U : Finset (ZMod (d * m))} {a b c : ZMod (d * m)} (h1 : bReach U a b) (h2 : bReach U b c) : bReach U a c

@[implicit_reducible]

noncomputable instance CriticalPortraits.bReachDecidable {d m : ℕ} (U : Finset (ZMod (d * m))) (a b : ZMod (d * m)) : Decidable (bReach U a b)

Equations

• CriticalPortraits.bReachDecidable U a b = Classical.dec (CriticalPortraits.bReach U a b)

noncomputable def CriticalPortraits.bVerts {d m : ℕ} (U : Finset (ZMod (d * m))) : Finset (ZMod (d * m))

The active vertices of β(U): the survivors and their balance parents.

Equations

• CriticalPortraits.bVerts U = U ∪ Finset.image (CriticalPortraits.betaParent U) U

noncomputable def CriticalPortraits.betaBlock {d m : ℕ} (U : Finset (ZMod (d * m))) (x : ZMod (d * m)) : Finset (ZMod (d * m))

The block of a point x: everything in bVerts U reachable from x.

Equations

• CriticalPortraits.betaBlock U x = {y ∈ CriticalPortraits.bVerts U | decide (CriticalPortraits.bReach U x y) = true}

theorem CriticalPortraits.mem_betaBlock {d m : ℕ} {U : Finset (ZMod (d * m))} {x y : ZMod (d * m)} : y ∈ betaBlock U x ↔ y ∈ bVerts U ∧ bReach U x y

noncomputable def CriticalPortraits.beta {d m : ℕ} (U : Finset (ZMod (d * m))) : Finset (Finset (ZMod (d * m)))

The balance forest β(U): the connected components of the parent edges.

Equations

• CriticalPortraits.beta U = Finset.image (CriticalPortraits.betaBlock U) (CriticalPortraits.bVerts U)

Layer 5: structural facts.

theorem CriticalPortraits.survivor_level_pos {d m : ℕ} (hd : 0 < d) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) : 1 ≤ u.val / m

Canonical U: every survivor has level ≥ 1 (canonicity at j = 0).

theorem CriticalPortraits.bAdj_sameFiber {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (_hcanon : LevelCanonical d m U) {a b : ZMod (d * m)} (h : bAdj U a b) : a.val % m = b.val % m

A single adjacency step preserves the fiber.

theorem CriticalPortraits.bReach_sameFiber {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {a b : ZMod (d * m)} (h : bReach U a b) : a.val % m = b.val % m

Reachability preserves the fiber.

Layer 6: Scount additivity and parent injectivity (I).

theorem CriticalPortraits.Scount_split {d m : ℕ} [NeZero (d * m)] {U : Finset (ZMod (d * m))} {x y : ℕ} {w : ZMod (d * m)} (hwU : w ∈ U) (hxw : x < w.val) (hwy : w.val < y) : Scount U x y = Scount U x w.val + 1 + Scount U w.val y

Scount split through an interior U-point w: if x < w.val < y and w ∈ U, then Scount U x y = Scount U x w.val + 1 + Scount U w.val y.

theorem CriticalPortraits.betaParent_balance {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) (hlu : 1 ≤ u.val / m) : ↑(Scount U (betaParent U u).val u.val) = ↑(u.val / m) - ↑(betaK U u) - 1

The balance identity at betaK: Scount U (betaParent).val u.val = lu - betaK - 1.

theorem CriticalPortraits.betaParent_inj {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u1 u2 : ZMod (d * m)} (hu1 : u1 ∈ U) (hu2 : u2 ∈ U) (heq : betaParent U u1 = betaParent U u2) : u1 = u2

Injectivity (I). The parent map is injective on survivors of canonical U.

Layer 7: the root function (descend to the non-U sink).

noncomputable def CriticalPortraits.bStep {d m : ℕ} (U : Finset (ZMod (d * m))) (x : ZMod (d * m)) : ZMod (d * m)

One descent step: parent if a survivor (level ≥ 1), else stay.

Equations

• CriticalPortraits.bStep U x = if _hx : x ∈ U then CriticalPortraits.betaParent U x else x

theorem CriticalPortraits.bStep_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x : ZMod (d * m)} (hx : x ∈ U) : (bStep U x).val < x.val

The step strictly decreases .val when x ∈ U.

@[irreducible]

noncomputable def CriticalPortraits.betaRoot {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) (x : ZMod (d * m)) : ZMod (d * m)

The root of x: iterate bStep until a non-U point. Well-founded on .val.

Equations

• CriticalPortraits.betaRoot hd hm hcanon x = if _hx : x ∈ U then CriticalPortraits.betaRoot hd hm hcanon (CriticalPortraits.betaParent U x) else x

theorem CriticalPortraits.betaRoot_of_not_mem {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x : ZMod (d * m)} (hx : x ∉ U) : betaRoot hd hm hcanon x = x

If x ∉ U, the root is x.

theorem CriticalPortraits.betaRoot_of_mem {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x : ZMod (d * m)} (hx : x ∈ U) : betaRoot hd hm hcanon x = betaRoot hd hm hcanon (betaParent U x)

If x ∈ U, the root descends to its parent's root.

theorem CriticalPortraits.betaRoot_not_mem {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) (x : ZMod (d * m)) : betaRoot hd hm hcanon x ∉ U

The root is never in U.

theorem CriticalPortraits.betaRoot_le {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) (x : ZMod (d * m)) : (betaRoot hd hm hcanon x).val ≤ x.val

The root's .val is ≤ x.val.

theorem CriticalPortraits.betaRoot_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x : ZMod (d * m)} (hx : x ∈ U) : (betaRoot hd hm hcanon x).val < x.val

For x ∈ U, the root is strictly below x.

theorem CriticalPortraits.bReach_betaRoot {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) (x : ZMod (d * m)) : bReach U x (betaRoot hd hm hcanon x)

x reaches its root.

theorem CriticalPortraits.betaRoot_bAdj {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x y : ZMod (d * m)} (h : bAdj U x y) : betaRoot hd hm hcanon x = betaRoot hd hm hcanon y

The root is invariant under one adjacency step.

theorem CriticalPortraits.betaRoot_bReach {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x y : ZMod (d * m)} (h : bReach U x y) : betaRoot hd hm hcanon x = betaRoot hd hm hcanon y

The root is invariant along reachability.

Layer 8: block membership and the min = root.

theorem CriticalPortraits.mem_bVerts_of_mem {d m : ℕ} {U : Finset (ZMod (d * m))} {x : ZMod (d * m)} (hx : x ∈ U) : x ∈ bVerts U

A U-point is a vertex.

theorem CriticalPortraits.betaParent_mem_bVerts {d m : ℕ} {U : Finset (ZMod (d * m))} {u : ZMod (d * m)} (hu : u ∈ U) : betaParent U u ∈ bVerts U

A balance parent of a U-point is a vertex.

theorem CriticalPortraits.bAdj_mem_bVerts {d m : ℕ} {U : Finset (ZMod (d * m))} {x y : ZMod (d * m)} (h : bAdj U x y) : y ∈ bVerts U

One adjacency step from a vertex lands on a vertex.

theorem CriticalPortraits.bReach_mem_bVerts {d m : ℕ} {U : Finset (ZMod (d * m))} {x y : ZMod (d * m)} (hx : x ∈ bVerts U) (h : bReach U x y) : y ∈ bVerts U

Reachability from a vertex stays in bVerts.

theorem CriticalPortraits.betaRoot_mem_bVerts {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x : ZMod (d * m)} (hx : x ∈ bVerts U) : betaRoot hd hm hcanon x ∈ bVerts U

The root of a vertex is a vertex.

theorem CriticalPortraits.betaRoot_mem_block {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x : ZMod (d * m)} (hx : x ∈ bVerts U) : betaRoot hd hm hcanon x ∈ betaBlock U x

The root is in the block of x.

theorem CriticalPortraits.betaRoot_min_in_block {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x y : ZMod (d * m)} (hy : y ∈ betaBlock U x) : (betaRoot hd hm hcanon x).val ≤ y.val

The root is .val-minimal in the block.

theorem CriticalPortraits.betaBlock_nonempty {d m : ℕ} {U : Finset (ZMod (d * m))} {x : ZMod (d * m)} (hx : x ∈ bVerts U) : (betaBlock U x).Nonempty

The block of a vertex is nonempty.

theorem CriticalPortraits.minVal_betaBlock {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x : ZMod (d * m)} (hx : x ∈ bVerts U) : minVal (betaBlock U x) ⋯ = betaRoot hd hm hcanon x

The minimum of a block is its root.

theorem CriticalPortraits.mem_U_of_mem_block_ne_root {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x y : ZMod (d * m)} (hy : y ∈ betaBlock U x) (hne : y ≠ betaRoot hd hm hcanon x) : y ∈ U

A block member that is not the root is a survivor (∈ U).

theorem CriticalPortraits.betaBlock_mem_beta {d m : ℕ} {U : Finset (ZMod (d * m))} {x : ZMod (d * m)} (hx : x ∈ bVerts U) : betaBlock U x ∈ beta U

betaBlock U x ∈ beta U for a vertex x.

theorem CriticalPortraits.mem_beta_iff {d m : ℕ} {U S : Finset (ZMod (d * m))} : S ∈ beta U ↔ ∃ v ∈ bVerts U, betaBlock U v = S

Layer 9: T(β U) = U.

theorem CriticalPortraits.T_beta {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) : T (beta U) = U

The load-bearing spec. T(β U) = U for canonical U.

Layer 10: β U is a Portrait — IsCriticalSet per block.

theorem CriticalPortraits.betaBlock_sameFiber {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x y : ZMod (d * m)} (hy : y ∈ betaBlock U x) : y.val % m = x.val % m

Every block member shares the vertex's fiber.

theorem CriticalPortraits.betaBlock_two_le {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {v : ZMod (d * m)} (hv : v ∈ bVerts U) : 2 ≤ (betaBlock U v).card

Every block contains a second point besides its root (its root has a U-child, or the vertex itself is a U-point).

theorem CriticalPortraits.betaBlock_critical {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {v : ZMod (d * m)} (hv : v ∈ bVerts U) : IsCriticalSet d m (betaBlock U v)

Each block is a critical set.

Layer 11: blocks determined by reachability; Disjoint.

theorem CriticalPortraits.betaBlock_eq_of_bReach {d m : ℕ} {U : Finset (ZMod (d * m))} {v1 v2 : ZMod (d * m)} (h : bReach U v1 v2) : betaBlock U v1 = betaBlock U v2

Reachable vertices have the same block.

theorem CriticalPortraits.betaBlock_disjoint {d m : ℕ} {U : Finset (ZMod (d * m))} {v1 v2 : ZMod (d * m)} (hne : betaBlock U v1 ≠ betaBlock U v2) : Disjoint (betaBlock U v1) (betaBlock U v2)

Distinct blocks are vertex-disjoint.

theorem CriticalPortraits.beta_pairwise_disjoint {d m : ℕ} {U : Finset (ZMod (d * m))} (A : Finset (ZMod (d * m))) : A ∈ beta U → ∀ B ∈ beta U, A ≠ B → Disjoint A B

Distinct blocks of β U are disjoint.

Layer 12: the weight identity ∑(|S|-1) = d-1.

theorem CriticalPortraits.beta_weight {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcard : U.card = d - 1) (hcanon : LevelCanonical d m U) : ∑ S ∈ beta U, (S.card - 1) = d - 1

Weight. ∑ S ∈ β U, (|S| - 1) = d - 1 (counted via T(β U) = U).

Layer 12b: M2 strict positivity past the balance index (the prefix bound).

theorem CriticalPortraits.Defc_pos_after {d m : ℕ} (_hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (_hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (_hu : u ∈ U) (hlu : 1 ≤ u.val / m) {j : ℕ} (hj1 : betaK U u < j) (hj2 : j ≤ u.val / m - 1) : 0 < Defc U (u.val % m) (u.val / m) u.val j

M2 strict positivity. For a survivor u of canonical U and betaK U u < j ≤ lu-1, the deficiency at j is strictly positive. If it were ≤ 0, then since D(lu-1) ≥ 0 (E1) and up-steps are ≤ 1, the discrete IVT on [j, lu-1] yields an exact zero > K, contradicting maximality betaK_max.

Layer 12c: the no-escape property P and the laminarity bridge to interval-closure.

theorem CriticalPortraits.betaK_ge {d m : ℕ} {U : Finset (ZMod (d * m))} {s : ZMod (d * m)} {k : ℕ} (hk : Defc U (s.val % m) (s.val / m) s.val k = 0) (hkle : k ≤ s.val / m - 1) : k ≤ betaK U s

Any balance index ≤ betaK: betaK is the largest zero of the deficiency.

theorem CriticalPortraits.Scount_add_le {d m : ℕ} (U : Finset (ZMod (d * m))) {x y z : ℕ} (hxy : x ≤ y) (hyz : y ≤ z) : Scount U x y + Scount U y z ≤ Scount U x z

Two disjoint open subintervals fit inside the whole: Scount is superadditive.

theorem CriticalPortraits.GPRE {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) (hlu : 1 ≤ u.val / m) {j : ℕ} (hj1 : betaK U u < j) (hj2 : j ≤ u.val / m) : ↑(Scount U (betaParent U u).val (u.val % m + j * m)) ≤ ↑j - ↑(betaK U u) - 1

GPRE prefix bound. For a survivor u of canonical U, with K := betaK U u and a φ-column index j with K < j ≤ lu, the survivor count from v*(u) up to the φ-point at level j is at most j - K - 1.

theorem CriticalPortraits.N0 {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) (hlu : 1 ≤ u.val / m) {t : ZMod (d * m)} (htU : t ∈ U) (hlo : (betaParent U u).val < t.val) (hhi : t.val < (betaParent U u).val + m) : False

N0. No survivor lies strictly inside one column-window above an edge bottom: there is no t ∈ U with v*(u) < t.val < v*(u) + m.

theorem CriticalPortraits.Scount_mono_right {d m : ℕ} (U : Finset (ZMod (d * m))) {x y y' : ℕ} (hyy : y ≤ y') : Scount U x y ≤ Scount U x y'

Shrinking the upper endpoint shrinks the open interval: Scount is monotone in y.

theorem CriticalPortraits.Q {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u s : ZMod (d * m)} (hu : u ∈ U) (hlu : 1 ≤ u.val / m) (hs : s ∈ U) (hslo : (betaParent U u).val < s.val) (hshi : s.val < u.val) {ly : ℕ} (hwlo : (betaParent U u).val ≤ s.val % m + ly * m) (hwhi : s.val % m + ly * m < (betaParent U u).val + m) : Defc U (s.val % m) (s.val / m) s.val ly ≤ 0

Q (the deficiency-sign anchor). For an edge (v,u) = (v*(u), u) and an interior survivor s (fiber ψ), if y = ψ + ly*m is the ψ-point in [v, v+m), then the deficiency of s at level ly is ≤ 0.

theorem CriticalPortraits.noEscape {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u s : ZMod (d * m)} (hu : u ∈ U) (hs : s ∈ U) (hslo : (betaParent U u).val < s.val) (hshi : s.val < u.val) : (betaParent U u).val ≤ (betaParent U s).val

P (no escape). For an edge (v,u) = (v*(u), u) of canonical U and an interior survivor s (v < s.val < u.val), the balance parent of s does not escape below v: v*(u).val ≤ v*(s).val.

theorem CriticalPortraits.root_ge {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {u : ZMod (d * m)} (hu : u ∈ U) (w : ZMod (d * m)) : w ∈ bVerts U → (betaParent U u).val < w.val → w.val < u.val → (betaParent U u).val ≤ (betaRoot hd hm hcanon w).val

The root stays above the edge bottom: for an edge (v,u) and any vertex w strictly inside its val-interval, the root of w has val ≥ v.

theorem CriticalPortraits.descend_cross {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) (L : ℕ) (w : ZMod (d * m)) : (betaRoot hd hm hcanon w).val ≤ L → L < w.val → ∃ b ∈ U, bReach U w b ∧ (betaParent U b).val ≤ L ∧ L < b.val

Descend across a threshold. If w is a vertex with betaRoot w ≤ L < w.val, then descending the parent chain crosses L: some survivor b reachable from w has v*(b).val ≤ L < b.val.

theorem CriticalPortraits.beta_interval_closed {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) {x z : ZMod (d * m)} (hx : x ∈ bVerts U) (hz : z ∈ bVerts U) (hne : betaBlock U x ≠ betaBlock U z) {p : ZMod (d * m)} (hp : p ∈ betaBlock U z) (hlo : (minVal (betaBlock U x) ⋯).val < p.val) (hhi : p.val < (maxVal (betaBlock U x) ⋯).val) (q : ZMod (d * m)) : q ∈ betaBlock U z → (minVal (betaBlock U x) ⋯).val ≤ q.val ∧ q.val ≤ (maxVal (betaBlock U x) ⋯).val

theorem CriticalPortraits.beta_unlinked {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcanon : LevelCanonical d m U) (A : Finset (ZMod (d * m))) : A ∈ beta U → ∀ B ∈ beta U, A ≠ B → Unlinked A B

Unlinked (N). Distinct blocks of β U are unlinked.

Layer 14: β U is a Portrait, and surjectivity.

theorem CriticalPortraits.beta_portrait {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {U : Finset (ZMod (d * m))} (hcard : U.card = d - 1) (hcanon : LevelCanonical d m U) : Portrait d m (beta U)

β(U) is a valid portrait.

theorem CriticalPortraits.T_surjOn {d m : ℕ} (hd : 0 < d) (hm : 0 < m) : Set.SurjOn T {P : Finset (Finset (ZMod (d * m))) | Portrait d m P} {U : Finset (ZMod (d * m)) | U.card = d - 1 ∧ LevelCanonical d m U}

Surjectivity. T is surjective onto canonical (d-1)-subsets.