INJECTIVITY of T (Brick 4).

T is injective on critical portraits, for every degree d:

T_injOn : Set.InjOn (T (N := d*m)) {P | Portrait d m P}

uses the REAL Portraits.T (= P.sup eraseMin) and Portraits.Portrait.

Bottom-up build (paper Part I — Uniqueness): PART A (AbstractLaminar) — the TIGHTNESS / equality layer on top of master (root_saturated, edge_tight_of_saturated) and COLUMN-SEPARATION (column_sep). PART B (CriticalPortraits) — geometric TIGHTNESS / column-sep at the survivor family, Lemma 2 (block-span laminarity), the BRIDGE edge core, the blocks-as-host-sets recovery, and the injectivity assembly.

STATUS: FULLY SORRY-FREE. The keystone predIn_forced (paper Part I, stage 1: the inductive forced-predecessor / Structural-Lemma dispatch — the documented all-d kernel) is now CLOSED for all d via the spanning-edge kernel (spanning_edge), built from the directional column separation (column_sep_with_gap / column_sep_geom_dir). Everything is axiom-clean ({propext, Classical.choice, Quot.sound}, NO sorryAx, NO native_decide), including: • PART A TIGHTNESS (root_saturated, edge_tight_of_saturated) and COLUMN-SEPARATION (column_sep, column_sep_with_gap) — degree-free, axiom-clean. • PART B geometric TIGHTNESS / column-sep (edge_tight_geom, column_sep_geom, column_sep_geom_dir), Lemma 2 (span_laminar), the BRIDGE edge core (bridge_edge). • Stage 1 keystone: predIn_forced — PROVED (strong induction on .val + WLOG + the spanning-edge crossing into no_alt). • Stage 2 (component recovery): hostSet_forced from predIn_forced. • The assembly T_inj / T_injOn.

PART A — TIGHTNESS in AbstractLaminar.

theorem AbstractLaminar.root_saturated {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} (hsat : N fam a b = b - a) (r : ι) : r ∈ Roots fam a b → N fam (fam.lo r) (fam.hi r) = fam.hi r - fam.lo r

Saturation propagates to roots. If the window (a,b] is saturated (N = b-a), then every root's subtree is itself saturated.

theorem AbstractLaminar.edge_tight_of_saturated {ι : Type u_1} [DecidableEq ι] (fam : Family ι) (w a b : ℕ) : b - a = w → N fam a b = b - a → ∀ e ∈ contained fam a b, N fam (fam.lo e) (fam.hi e) = fam.hi e - fam.lo e

Every edge is tight. If the window (a,b] is saturated, then every edge contained in it has a saturated own-window (N(lo e, hi e) = hi e - lo e, i.e. g(e) = h(e) - 1).

A2 — COLUMN-SEPARATION.

For a saturated window (a,b] whose top edge e0 exists (interval exactly (a,b]), every root r has col r ≠ col e0. Proof by the seam scan: the gap splits roots into a left run (each shares the bottom a up to the gap; bLeft/bSeam ⇒ col e0 < col r) and a right run (each shares the top b down to the gap; bRight/bSeam ⇒ col r < col e0).

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

Saturated window with a top edge: the root subtree widths sum to exactly b - a - 1.

theorem AbstractLaminar.exists_gap {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} (hab : a < b) (hsat : N fam a b = b - a) (htop : (topEdges fam a b).Nonempty) : ∃ (g : ℕ), a < g ∧ g ≤ b ∧ ∀ r ∈ Roots fam a b, ¬(fam.lo r < g ∧ g ≤ fam.hi r)

The root level-intervals of a saturated top-edged window miss exactly one level g*: there is a unique g ∈ (a,b] covered by no root.

theorem AbstractLaminar.covered_of_ne_gap {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b g : ℕ} (htop : (topEdges fam a b).Nonempty) (hsat : N fam a b = b - a) (hab : a < b) (hg1 : a < g) (hg2 : g ≤ b) (hgap : ∀ r ∈ Roots fam a b, ¬(fam.lo r < g ∧ g ≤ fam.hi r)) {t : ℕ} (ht1 : a < t) (ht2 : t ≤ b) (htne : t ≠ g) : ∃ r ∈ Roots fam a b, fam.lo r < t ∧ t ≤ fam.hi r

Every level in (a,b] except the gap g (with a < g ≤ b) is covered by some root.

theorem AbstractLaminar.seam_of_adjacent {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} {r'' r : ι} (hr'' : r'' ∈ Roots fam a b) (hr : r ∈ Roots fam a b) {s : ℕ} (hs1 : fam.lo r'' < s) (hs2 : s ≤ fam.hi r'') (hrhi : s + 1 ≤ fam.hi r) (hadj : fam.lo r = s) : fam.hi r'' = s

Distinct roots covering adjacent levels seam: if r'' covers s and r covers a level just above s (with lo r < s+1), and r'' ≠ r, then hi r'' = lo r. (Used in the seam scan.)

theorem AbstractLaminar.column_sep {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} (hab : a < b) (hsat : N fam a b = b - a) {e0 : ι} (he0E : e0 ∈ fam.E) (he0lo : fam.lo e0 = a) (he0hi : fam.hi e0 = b) (r : ι) : r ∈ Roots fam a b → fam.col r ≠ fam.col e0

COLUMN-SEPARATION (abstract). For a saturated window (a,b] with a top edge e0, every root has column ≠ col e0.

theorem AbstractLaminar.column_sep_with_gap {ι : Type u_1} [DecidableEq ι] (fam : Family ι) {a b : ℕ} (hab : a < b) (hsat : N fam a b = b - a) {e0 : ι} (he0E : e0 ∈ fam.E) (he0lo : fam.lo e0 = a) (he0hi : fam.hi e0 = b) : ∃ (g : ℕ), a < g ∧ g ≤ b ∧ (∀ r ∈ Roots fam a b, ¬(fam.lo r < g ∧ g ≤ fam.hi r)) ∧ (∀ r ∈ Roots fam a b, fam.hi r < g → fam.col e0 < fam.col r) ∧ ∀ r ∈ Roots fam a b, g ≤ fam.lo r → fam.col r < fam.col e0

DIRECTIONAL COLUMN-SEPARATION (abstract). As column_sep, but exposes the gap g together with the run-direction columns: left roots (top below the gap) have col e0 < col r, right roots (bottom above the gap) have col r < col e0.

PART B — geometric layer in CriticalPortraits.

B0. blocks = host sets: P = image (survivor ↦ hostSet).

theorem CriticalPortraits.hostSet_eq_of_mem_eraseMin {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {S : Finset (ZMod (d * m))} (hS : S ∈ P) {x : ZMod (d * m)} (hxe : x ∈ eraseMin S) : hostSet P x ⋯ = S

Each block of a portrait is the host set of any of its survivors. More precisely: if x ∈ eraseMin S and S ∈ P then hostSet P x = S (the survivor's recovered home is its block, by portrait disjointness).

theorem CriticalPortraits.portrait_eq_image_hostSet {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) : P = Finset.image (fun (x : ↥(T P)) => hostSet P ↑x ⋯) (T P).attach

P is recovered as the image of its survivors' host sets.

B1. Geometric TIGHTNESS and COLUMN-SEPARATION for the survivor family.

We instantiate the abstract TIGHTNESS at the real survivorFamily. The window (0, d-1] is saturated (N = d-1) because every survivor's level lies in [0, d-1] — 0 ≤ loV and hiV ≤ d-1, so all d-1 edges are contained, and the window width is d-1.

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

Every survivor's level is < d (hence hiV x ≤ d - 1).

theorem CriticalPortraits.survivorFamily_contained_eq {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) : AbstractLaminar.contained (survivorFamily hd hm hP) 0 (d - 1) = T P

The window (0, d-1] contains every edge of the survivor family.

theorem CriticalPortraits.survivorFamily_saturated {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) : AbstractLaminar.N (survivorFamily hd hm hP) 0 (d - 1) = d - 1 - 0

Geometric saturation. N (survivorFamily) 0 (d-1) = d - 1.

theorem CriticalPortraits.edge_tight_geom {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e : ZMod (d * m)} (he : e ∈ T P) : AbstractLaminar.N (survivorFamily hd hm hP) (loV P e) (hiV e) = hiV e - loV P e

Geometric TIGHTNESS (g(e) = h(e) - 1). Every survivor edge e has a saturated own window: N(loV e, hiV e) = hiV e - loV e.

theorem CriticalPortraits.column_sep_geom {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e : ZMod (d * m)} (he : e ∈ T P) (hwin : loV P e < hiV e) (r : ZMod (d * m)) : r ∈ AbstractLaminar.Roots (survivorFamily hd hm hP) (loV P e) (hiV e) → colV r ≠ colV e

Geometric COLUMN-SEPARATION. For a survivor edge e with a nondegenerate own window, every maximal nested tile (root of (loV e, hiV e]) has column ≠ colV e.

theorem CriticalPortraits.column_sep_geom_dir {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {e : ZMod (d * m)} (he : e ∈ T P) (hwin : loV P e < hiV e) : ∃ (g : ℕ), loV P e < g ∧ g ≤ hiV e ∧ (∀ r ∈ AbstractLaminar.Roots (survivorFamily hd hm hP) (loV P e) (hiV e), ¬(loV P r < g ∧ g ≤ hiV r)) ∧ (∀ r ∈ AbstractLaminar.Roots (survivorFamily hd hm hP) (loV P e) (hiV e), hiV r < g → colV e < colV r) ∧ ∀ r ∈ AbstractLaminar.Roots (survivorFamily hd hm hP) (loV P e) (hiV e), g ≤ loV P r → colV r < colV e

Geometric DIRECTIONAL COLUMN-SEPARATION. Exposes the gap level and the run-direction columns at the survivor family.

B2. Block spans and Lemma 2 (span laminarity).

spanLo S, spanHi S are the .val of the lowest/highest points of a block S. Lemma 2 says distinct blocks' spans are laminar (nested or disjoint), proved directly from Unlinked

• the alternation witness linked_of_lt (structurally identical to lemmaA/cross_false).

noncomputable def CriticalPortraits.maxVal {N : ℕ} (S : Finset (ZMod N)) (h : S.Nonempty) : ZMod N

The greatest-.val element of a nonempty set.

Equations

• CriticalPortraits.maxVal S h = ⋯.choose

theorem CriticalPortraits.maxVal_mem {N : ℕ} (S : Finset (ZMod N)) (h : S.Nonempty) : maxVal S h ∈ S

theorem CriticalPortraits.maxVal_ge {N : ℕ} (S : Finset (ZMod N)) (h : S.Nonempty) (x : ZMod N) : x ∈ S → x.val ≤ (maxVal S h).val

noncomputable def CriticalPortraits.spanLo {N : ℕ} (S : Finset (ZMod N)) (h : S.Nonempty) : ℕ

The .val-span of a block: [minVal, maxVal].

Equations

• CriticalPortraits.spanLo S h = (CriticalPortraits.minVal S h).val

noncomputable def CriticalPortraits.spanHi {N : ℕ} (S : Finset (ZMod N)) (h : S.Nonempty) : ℕ

The greatest .val attained on a nonempty finset S.

Equations

• CriticalPortraits.spanHi S h = (CriticalPortraits.maxVal S h).val

theorem CriticalPortraits.span_laminar {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {A B : Finset (ZMod (d * m))} (hA : A ∈ P) (hB : B ∈ P) (hAB : A ≠ B) (hAne : A.Nonempty) (hBne : B.Nonempty) : ¬(spanLo A hAne < spanLo B hBne ∧ spanLo B hBne < spanHi A hAne ∧ spanHi A hAne < spanHi B hBne)

Lemma 2 (span laminarity). Distinct blocks of a portrait have laminar spans: nested or disjoint (no proper .val-overlap spanLo A < spanLo B < spanHi A < spanHi B).

theorem CriticalPortraits.mem_span {N : ℕ} {S : Finset (ZMod N)} (h : S.Nonempty) {x : ZMod N} (hx : x ∈ S) : spanLo S h ≤ x.val ∧ x.val ≤ spanHi S h

Lemma 2 (hull edge). Every block element's .val lies within the span.

B3. The BRIDGE (edge core).

The algebraic heart of the Structural Lemma: a same-column edge strictly nested inside u's edge is NOT a maximal tile (its rootS is a strictly-enclosing edge of a DIFFERENT column). This is exactly "the c*-block B strictly inside (w,u) is enclosed by an in-gap block of column ≠ c*", phrased in the edge model. Proved from column_sep_geom + the rootS machinery.

theorem CriticalPortraits.bridge_edge {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {u b2 : ZMod (d * m)} (hu : u ∈ T P) (hb2 : b2 ∈ T P) (hcol : colV b2 = colV u) (hlo : loV P u < loV P b2) (hhi : hiV b2 < hiV u) : ∃ g ∈ T P, colV g ≠ colV u ∧ loV P u ≤ loV P g ∧ loV P g ≤ loV P b2 ∧ hiV b2 ≤ hiV g ∧ hiV g ≤ hiV u ∧ g ≠ b2

BRIDGE (edge form). If a survivor b2 (same column as u) has its edge strictly nested inside u's edge, then there is a survivor g of a DIFFERENT column whose edge encloses b2's and is nested in u's: loV u ≤ loV g ≤ loV b2, hiV b2 ≤ hiV g ≤ hiV u, colV g ≠ colV u, and g ≠ b2.

B-keystone (stage 1): the predecessor of each survivor is FORCED by U = T P.

This is the genuinely deep all-d kernel — the inductive forced-predecessor dispatch that consumes the now-proved bridge_edge / column_sep_geom / edge_tight_geom / span_laminar. It is now PROVED (no sorry); the stage-2 component recovery hostSet_forced below depends on it.

Helper lemmas for predIn_forced.

theorem CriticalPortraits.level_lt_of_val_lt {d m : ℕ} [NeZero (d * m)] {x y : ZMod (d * m)} (hfib : x.val % m = y.val % m) (h : x.val < y.val) : x.val / m < y.val / m

Same-fiber .val comparison is the level comparison (strict).

theorem CriticalPortraits.root_val_lt {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {g x : ZMod (d * m)} (hg : g ∈ T P) (hx : x ∈ T P) (hlo : loV P x ≤ loV P g) (hhi : hiV g ≤ hiV x) (hcol : colV g ≠ colV x) : g.val < x.val

A strict root g of x's window (so loV P x ≤ loV P g, hiV g ≤ hiV x, colV g ≠ colV x) has g.val < x.val.

theorem CriticalPortraits.spanning_edge {d m : ℕ} [NeZero (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) {ℓ : ℕ} (hℓ1 : loV P x < ℓ) (hℓ2 : ℓ < hiV x) : ∃ (b : ZMod (d * m)) (hb : b ∈ T P), colV b ≠ colV x ∧ (predIn P b hb).val < colV x + ℓ * m ∧ colV x + ℓ * m < b.val ∧ b.val < x.val

The spanning-edge kernel. In one portrait P, for a survivor x and a level ℓ strictly inside x's own window (loV P x, hiV x), there is a survivor b of a different column than x whose edge straddles the value colV x + ℓ * m: (predIn P b _).val < colV x + ℓ*m < b.val < x.val.

This is the formalized Structural Lemma / Bridge content: the value v₀ = colV x + ℓ*m (a same-fiber position strictly inside x's edge) is crossed by some maximal nested tile of a different column. Proved from saturation (edge_tight_geom), column-separation (column_sep_geom), and the gap/cover/seam machinery.

theorem CriticalPortraits.predIn_forced {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P₁ P₂ : Finset (Finset (ZMod (d * m)))} (h₁ : Portrait d m P₁) (h₂ : Portrait d m P₂) (hT : T P₁ = T P₂) {x : ZMod (d * m)} (hx₁ : x ∈ T P₁) (hx₂ : x ∈ T P₂) : predIn P₁ x hx₁ = predIn P₂ x hx₂

B-keystone (stage 2): host blocks are forced by U and the forced predecessors.

Stage 2 is sorry-free. A block is recovered as the connected component of its survivors under the immediate-predecessor (edgeStep) relation, together with its unique non-survivor minVal (the "root"). Since T P and (by predIn_forced) the predIn map agree across P₁, P₂, the edgeStep relation agrees, hence components and roots agree, hence host blocks agree.

theorem CriticalPortraits.hostSet_eq_of_mem {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {u : ZMod (d * m)} (hu : u ∈ T P) {S : Finset (ZMod (d * m))} (hSP : S ∈ P) (huS : u ∈ S) : hostSet P u hu = S

hostSet P u is THE block containing the survivor u.

theorem CriticalPortraits.minVal_congr {N : ℕ} {S S' : Finset (ZMod N)} (hS : S.Nonempty) (hS' : S'.Nonempty) (h : S = S') : minVal S hS = minVal S' hS'

minVal only depends on the set (proof-irrelevant nonemptiness witness).

theorem CriticalPortraits.minVal_host_not_mem_T {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x : ZMod (d * m)} (hx : x ∈ T P) (hne : (hostSet P x hx).Nonempty) : minVal (hostSet P x hx) hne ∉ T P

The dropped point of a block is not a survivor of P (blocks are disjoint).

def CriticalPortraits.edgeStep {d m : ℕ} [NeZero (d * m)] (P : Finset (Finset (ZMod (d * m)))) (u v : ZMod (d * m)) : Prop

The same-block immediate-predecessor step relation on survivors: determined by T P + predIn.

Equations

• CriticalPortraits.edgeStep P u v = ∃ (hu : u ∈ CriticalPortraits.T P) (hv : v ∈ CriticalPortraits.T P), CriticalPortraits.predIn P u hu = v ∨ CriticalPortraits.predIn P v hv = u

theorem CriticalPortraits.edgeStep_symm {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {u v : ZMod (d * m)} (h : edgeStep P u v) : edgeStep P v u

theorem CriticalPortraits.reach_symm {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} {u v : ZMod (d * m)} (h : Relation.ReflTransGen (edgeStep P) u v) : Relation.ReflTransGen (edgeStep P) v u

theorem CriticalPortraits.edgeStep_sameHost {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {u v : ZMod (d * m)} (hstep : edgeStep P u v) (hu : u ∈ T P) (hv : v ∈ T P) : hostSet P u hu = hostSet P v hv

An edgeStep keeps you in the same host (the predecessor lives in the same block).

theorem CriticalPortraits.hostSet_predIn {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {u : ZMod (d * m)} (hu : u ∈ T P) (hpu : predIn P u hu ∈ T P) : hostSet P (predIn P u hu) hpu = hostSet P u hu

For a survivor u whose predecessor is itself a survivor, they share a host.

theorem CriticalPortraits.reach_sameHost {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x z : ZMod (d * m)} (hx : x ∈ T P) (hreach : Relation.ReflTransGen (edgeStep P) x z) (hz : z ∈ T P) : hostSet P z hz = hostSet P x hx

Survivors reachable from x by edgeStep share x's host.

theorem CriticalPortraits.reach_to_low {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) (n : ℕ) (z : ZMod (d * m)) : z.val = n → ∀ (hz : z ∈ T P), ∃ (q : ZMod (d * m)) (hq : q ∈ T P), predIn P q hq ∉ T P ∧ hostSet P q hq = hostSet P z hz ∧ Relation.ReflTransGen (edgeStep P) z q

Every survivor z reaches the bottom survivor q of its block (predecessor a non-survivor).

theorem CriticalPortraits.reach_of_sameHost {d m : ℕ} [NeZero (d * m)] {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) {x z : ZMod (d * m)} (hx : x ∈ T P) (hz : z ∈ T P) (hhost : hostSet P z hz = hostSet P x hx) : Relation.ReflTransGen (edgeStep P) z x

Two survivors in the same host reach the SAME bottom survivor; hence are mutually reachable.

theorem CriticalPortraits.edgeStep_forced {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P₁ P₂ : Finset (Finset (ZMod (d * m)))} (h₁ : Portrait d m P₁) (h₂ : Portrait d m P₂) (hT : T P₁ = T P₂) {u v : ZMod (d * m)} (hstep : edgeStep P₁ u v) : edgeStep P₂ u v

With forced predecessors and equal survivor sets, the edgeStep relations agree.

theorem CriticalPortraits.reach_forced {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P₁ P₂ : Finset (Finset (ZMod (d * m)))} (h₁ : Portrait d m P₁) (h₂ : Portrait d m P₂) (hT : T P₁ = T P₂) {u v : ZMod (d * m)} (hreach : Relation.ReflTransGen (edgeStep P₁) u v) : Relation.ReflTransGen (edgeStep P₂) u v

Reachability transfers between portraits with forced predecessors.

B-keystone: the host sets are forced by the survivor set U = T P.

This is exactly Part I (Uniqueness) of the paper: a critical portrait is reconstructible from its survivor set. All of the structural content (TIGHTNESS, Column-Separation, the Bridge / Structural Lemma, and the resulting "predecessor forced ⇒ block forced") lives here.

theorem CriticalPortraits.hostSet_forced {d m : ℕ} [NeZero (d * m)] (hd : 0 < d) (hm : 0 < m) {P₁ P₂ : Finset (Finset (ZMod (d * m)))} (h₁ : Portrait d m P₁) (h₂ : Portrait d m P₂) (hT : T P₁ = T P₂) {x : ZMod (d * m)} (hx₁ : x ∈ T P₁) (hx₂ : x ∈ T P₂) : hostSet P₁ x hx₁ = hostSet P₂ x hx₂

KEYSTONE (Part I uniqueness) — now PROVED (sorry-free).

If two portraits have the same survivor set, then each survivor's host block is the same in both. This is exactly the paper's Part I ("T injective ↔ the portrait is reconstructible from U"), the documented open all-d kernel (machine-verified d ≤ 8; never previously mechanized for all d). Its proof has two stages, both genuinely deep:

(1) predIn forced. ∀ u ∈ U, predIn P₁ u = predIn P₂ u. By induction over .val order: w = predIn P u is the GREEDY pick from U — the highest same-fiber v < u that is unused and whose chord (v,u) crosses no already-committed (lower-.val) edge. Every higher candidate v ∈ (w,u) is illegal: either v ∈ U (a non-top of its block; its child is left of u, already committed) or, by the Structural Lemma / Bridge, v's block is not maximal in (w,u), so it sits in the gap of an enclosing block whose edge (a,b) has a < v < b < u, crossing the committed (a,b). The Structural Lemma ("no block maximal in a parent-gap (w,u) has its top in fiber(u)") is fed by the now-PROVED substrate: • TIGHTNESS : edge_tight_geom (g(e) = h(e) - 1). • COLUMN-SEP : column_sep_geom (no maximal tile of e shares e's column). • BRIDGE : bridge_edge (PROVED) — the c*-edge eB of a c*-block B strictly inside (w,u) is non-maximal, so eB ≪ a maximal tile g with col g ≠ c*. Remaining glue: span_laminar (Lemma 2, PROVED) + chord-enclosure (sep_master) ⇒ block(g) strictly encloses span(B) ⇒ B not maximal.

(2) Block forced from predIn. Edges {(predIn u, u) : u ∈ U} are then equal across P₁, P₂; the host block of x is the connected component of x in the predecessor graph (hostSet P x = {minVal} ∪ {survivors with the same predIn-descent root}), so equal edges ⇒ equal components ⇒ equal host blocks.

PROVED and available: edge_tight_geom (TIGHTNESS), column_sep_geom (COLUMN-SEP), span_laminar (Lemma 2), bridge_edge (BRIDGE edge core), plus all of Forward's edge model (predIn_*, no_alt, lemmaA/B, survivorFamily).

This theorem is now SORRY-FREE: stage (2) (component recovery) is fully proved here from predIn_forced (stage 1, the single remaining sorry). A block is recovered as the edgeStep-component of its survivors together with its unique non-survivor minVal root; both are forced because T P and the predIn map agree across P₁, P₂.

B-assembly: T injective.

theorem CriticalPortraits.T_inj {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {P₁ P₂ : Finset (Finset (ZMod (d * m)))} (h₁ : Portrait d m P₁) (h₂ : Portrait d m P₂) (hT : T P₁ = T P₂) : P₁ = P₂

INJECTIVITY (implication form). Two portraits with equal survivor sets are equal.

theorem CriticalPortraits.T_injOn {d m : ℕ} (hd : 0 < d) (hm : 0 < m) : Set.InjOn T {P : Finset (Finset (ZMod (d * m))) | Portrait d m P}

INJECTIVITY (Set.InjOn form, the stated target).