Geometric foundation: the critical-portrait model on ZMod (d*m).

A faithful, proof-friendly port of the bare-Lean verified model (LamKit.CriticalCensusGeneral; native_decide-verified d = 3..6). Mathlib has cyclic betweenness (Order.Circular) but no chords/linking/laminar API, so this is built from scratch.

• IsCriticalSet — subset of one σ_d-fiber, ≥ 2 points (weight |S| - 1).
• Linked / Unlinked — convex hulls cross / don't cross on the .val-circle. Unlinked is the negation of an alternating crossing quadruple; it agrees with the bare-Lean hullsUnlinked test (cyclicRuns ≤ 1) on every instance (verified #evals match the census 5/14/12/55/22/42).
• Portrait — pairwise vertex-disjoint, pairwise-unlinked critical sets, weight d-1.
• T — delete the lowest-level (= least .val) point of each set, union all.

API proved here (sorry-free, native_decide-free, real kernel proofs):

• T_card — the weight identity #T(P) = d - 1.
• Decidable instances throughout; an unconditional Fintype for the portrait subtype.
• Downstream hooks: sep_master (the master separation inequality (M)), linked_of_lt, mem_T, the minVal spec lemmas.

Positions/level/fiber/LevelCanonical are reused from CriticalPortraits.Core. The forward goal LevelCanonical (T P) is a LATER brick (3b) and is deliberately NOT stated here.

1. Critical sets.

def CriticalPortraits.IsCriticalSet (d m : ℕ) (S : Finset (ZMod (d * m))) : Prop

S ⊆ Z_{d*m} is a critical set: it lies in one σ_d-fiber (all points share a column r < m) and has at least 2 points. Its weight is S.card - 1.

Equations

• CriticalPortraits.IsCriticalSet d m S = ((∃ r < m, ∀ x ∈ S, x.val % m = r) ∧ 2 ≤ S.card)

@[implicit_reducible]

instance CriticalPortraits.instDecidableIsCriticalSet (d m : ℕ) (S : Finset (ZMod (d * m))) : Decidable (IsCriticalSet d m S)

Equations

• CriticalPortraits.instDecidableIsCriticalSet d m S = id inferInstance

2. Unlinked: convex hulls don't cross.

Linked A B says there are two chords — (a1, a2) with endpoints in A, (b1, b2) with endpoints in B — that cross on the circle Z_N read by .val. Geometrically the two crossing patterns (up to relabelling) are a1 < b1 < a2 < b2 and b1 < a1 < b2 < a2 (strict on .val). This is the val-linear form of "the four points alternate cyclically a, b, a, b", which is exactly the negation of "A is a single cyclic run" — i.e. the bare-Lean hullsUnlinked test cyclicRuns ≤ 1. Unlinked A B := ¬ Linked A B.

def CriticalPortraits.Linked {N : ℕ} (A B : Finset (ZMod N)) : Prop

Two cyclic subsets A and B are linked when they interleave.

Equations

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

@[implicit_reducible]

instance CriticalPortraits.instDecidableLinked {N : ℕ} (A B : Finset (ZMod N)) : Decidable (Linked A B)

Equations

• CriticalPortraits.instDecidableLinked A B = id inferInstance

def CriticalPortraits.Unlinked {N : ℕ} (A B : Finset (ZMod N)) : Prop

A and B have unlinked convex hulls (no crossing chords).

Equations

• CriticalPortraits.Unlinked A B = ¬CriticalPortraits.Linked A B

@[implicit_reducible]

instance CriticalPortraits.instDecidableUnlinked {N : ℕ} (A B : Finset (ZMod N)) : Decidable (Unlinked A B)

Equations

• CriticalPortraits.instDecidableUnlinked A B = id inferInstance

theorem CriticalPortraits.Unlinked.symm {N : ℕ} {A B : Finset (ZMod N)} (h : Unlinked A B) : Unlinked B A

Unlinked is symmetric: crossing chords of A, B are crossing chords of B, A.

theorem CriticalPortraits.not_unlinked_of_alternating {N : ℕ} {A B : Finset (ZMod N)} {a1 a2 b1 b2 : ZMod N} (ha1 : a1 ∈ A) (ha2 : a2 ∈ A) (hb1 : b1 ∈ B) (hb2 : b2 ∈ B) (h1 : a1.val < b1.val) (h2 : b1.val < a2.val) (h3 : a2.val < b2.val) : ¬Unlinked A B

The crossing witness Lemma A / Seam / Bridge will call: a strictly-alternating quadruple a1 < b1 < a2 < b2 (linear .val order) with a1,a2 ∈ A, b1,b2 ∈ B contradicts Unlinked A B.

3. Critical portraits.

def CriticalPortraits.Portrait (d m : ℕ) (P : Finset (Finset (ZMod (d * m)))) : Prop

A critical portrait: a family of critical sets that is pairwise vertex-disjoint, pairwise unlinked, of total weight ∑ (|S| - 1) = d - 1.

Equations

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

@[implicit_reducible]

instance CriticalPortraits.instDecidablePortrait (d m : ℕ) (P : Finset (Finset (ZMod (d * m)))) : Decidable (Portrait d m P)

Equations

• CriticalPortraits.instDecidablePortrait d m P = id inferInstance

4. The portrait subtype is a Fintype (unconditional, mirroring instFiniteCanonical).

theorem CriticalPortraits.portrait_eq_empty_of_degenerate (d m : ℕ) (h0 : d * m = 0) (P : Finset (Finset (ZMod (d * m)))) (hP : Portrait d m P) : P = ∅

When d * m = 0, no portrait exists. (m = 0 ⇒ no fiber witness; d = 0 ⇒ weight target 0, but every critical set has positive weight, so the family is empty.)

instance CriticalPortraits.instFinitePortrait (d m : ℕ) : Finite { P : Finset (Finset (ZMod (d * m))) // Portrait d m P }

@[implicit_reducible]

noncomputable instance CriticalPortraits.instFintypePortrait (d m : ℕ) : Fintype { P : Finset (Finset (ZMod (d * m))) // Portrait d m P }

Equations

• CriticalPortraits.instFintypePortrait d m = Fintype.ofFinite { P : Finset (Finset (ZMod (d * m))) // CriticalPortraits.Portrait d m P }

5. The delete-min map T.

ZMod N has no LinearOrder, so we pick the dropped point by minimising .val via Finset.exists_min_image. Within a single fiber val = level*m + col is strictly monotone in level, so least-.val = lowest-level = exactly bare-Lean's S.drop 1.

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

The least-.val element of a nonempty set (the lowest-level point of a critical set).

Equations

• CriticalPortraits.minVal S h = ⋯.choose

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

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

noncomputable def CriticalPortraits.eraseMin {N : ℕ} (S : Finset (ZMod N)) : Finset (ZMod N)

Drop the lowest-level (least-.val) point of S (identity on the empty set).

Equations

• CriticalPortraits.eraseMin S = if h : S.Nonempty then S.erase (CriticalPortraits.minVal S h) else S

theorem CriticalPortraits.eraseMin_subset {N : ℕ} (S : Finset (ZMod N)) : eraseMin S ⊆ S

theorem CriticalPortraits.eraseMin_card {N : ℕ} (S : Finset (ZMod N)) (h : S.Nonempty) : (eraseMin S).card = S.card - 1

theorem CriticalPortraits.mem_eraseMin {N : ℕ} (S : Finset (ZMod N)) (h : S.Nonempty) (x : ZMod N) : x ∈ eraseMin S ↔ x ∈ S ∧ x ≠ minVal S h

Membership in eraseMin: everything of S except its .val-minimum (nonempty S). The clean characterization the downstream membership reasoning will use.

noncomputable def CriticalPortraits.T {N : ℕ} (P : Finset (Finset (ZMod N))) : Finset (ZMod N)

T(P): delete the lowest-level point of every set, then take the union.

Equations

• CriticalPortraits.T P = P.sup CriticalPortraits.eraseMin

theorem CriticalPortraits.eraseMin_pairwiseDisjoint {d m : ℕ} (P : Finset (Finset (ZMod (d * m)))) (hP : Portrait d m P) : (↑P).PairwiseDisjoint eraseMin

The erased sets remain pairwise disjoint (erase only shrinks).

6. BASIC API: the weight identity #T = d - 1.

theorem CriticalPortraits.T_card {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) : (T P).card = d - 1

The weight identity. For a critical portrait, #T(P) = d - 1.

6b. The min-rule is the min-LEVEL rule (load-bearing for forward/surjectivity).

The bare-Lean S.drop 1 drops the lowest-LEVEL point. minVal drops the least-.val point. These coincide on a critical set because within one fiber the .val order is the level order, and the level is injective on the set. This underwrites "survivors = edge tops" and "each block/component has a unique non-survivor = its lowest-level vertex" (scout risk R2).

theorem CriticalPortraits.val_le_iff_level_le_of_sameFiber {N m : ℕ} {x y : ZMod N} (hxy : x.val % m = y.val % m) : x.val ≤ y.val ↔ x.val / m ≤ y.val / m

Within a single fiber (same residue mod m), the .val order equals the level order.

theorem CriticalPortraits.level_injOn_fiber {N m : ℕ} [NeZero N] {x y : ZMod N} (hxy : x.val % m = y.val % m) (hlev : x.val / m = y.val / m) : x = y

The level is injective on a single fiber: same fiber + same level ⇒ same .val ⇒ same element.

theorem CriticalPortraits.minVal_level_le {d m : ℕ} {S : Finset (ZMod (d * m))} (hS : IsCriticalSet d m S) (h : S.Nonempty) (x : ZMod (d * m)) : x ∈ S → (minVal S h).val / m ≤ x.val / m

The min-rule is the min-LEVEL rule. On a critical set, minVal S is the unique point of minimum level: its level is ≤ every member's.

theorem CriticalPortraits.minVal_lt_survivor {d m : ℕ} (hd : 0 < d) (hm : 0 < m) {S : Finset (ZMod (d * m))} (hS : IsCriticalSet d m S) (h : S.Nonempty) (x : ZMod (d * m)) : x ∈ eraseMin S → (minVal S h).val / m < x.val / m

The dropped point (the minimum) is strictly below — in LEVEL — every survivor of that set. This is what makes "survivors = edge tops" hold; each critical set keeps exactly its tops.

7. Helper facts the downstream bricks will want.

These pin the model to the verified one and expose the (M)-style arithmetic.

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

Within one fiber, val is strictly monotone in level: a point's .val equals level * m + col. (Used to identify least-.val with lowest-level.)

theorem CriticalPortraits.sep_master {m p q a c : ℕ} (hp : p < m) (_hq : q < m) (hac : a < c) : p + a * m < q + c * m

The master separation inequality (M). One level of separation beats any column offset: for columns p, q < m and levels a < c, p + a*m < q + c*m.

theorem CriticalPortraits.linked_of_lt {N : ℕ} {A B : Finset (ZMod N)} {a1 a2 b1 b2 : ZMod N} (ha1 : a1 ∈ A) (ha2 : a2 ∈ A) (hb1 : b1 ∈ B) (hb2 : b2 ∈ B) (h1 : a1.val < b1.val) (h2 : b1.val < a2.val) (h3 : a2.val < b2.val) : Linked A B

A crossing quadruple in strict val-order makes A, B linked (the (M)-witness hook).

theorem CriticalPortraits.mem_T {N : ℕ} {P : Finset (Finset (ZMod N))} {x : ZMod N} : x ∈ T P ↔ ∃ S ∈ P, x ∈ eraseMin S

Membership in T P.

8. T P lands in the (d-1)-subsets (the start of the Tsub packaging).

T_card gives the cardinality; we package T P into the same {S // S.card = d-1} subtype the denominator counts (Denominator.Asub). The remaining LevelCanonical (T P) clause — landing in the FULL {S // S.card = d-1 ∧ LevelCanonical d m S} subtype (Denominator.Csub) — is the FORWARD direction (brick 3b) and is deliberately NOT proved here.

noncomputable def CriticalPortraits.TsubCard {d m : ℕ} {P : Finset (Finset (ZMod (d * m)))} (hP : Portrait d m P) : { S : Finset (ZMod (d * m)) // S.card = d - 1 }

T P packaged as a (d-1)-subset; the first half of the eventual Tsub into Denominator.Csub.

Equations

• CriticalPortraits.TsubCard hP = ⟨CriticalPortraits.T P, ⋯⟩