Section 7 corrected foundation: first non-scalar chief factor + ⊆-minimal kernel

Manuscript-verification pass (2026-07-01) found the §7 kernel interface makes three statements STRONGER than the manuscript proves (PROGRESS.md "SOUNDNESS FINDINGS"):

1. the manuscript chooses S ◁ P with all chief factors below S scalar and V = P/S the first non-scalar factor (l.3616–3623) — NonScalarChiefFactor records no such condition, and lem:collapse genuinely needs it (the [S,Ñ] = 1 coprime step);
2. the manuscript chooses K ◁ Y, K ≤ P, minimal subject to KS = P — the interface field minimal_K asserts least (Ksub ≤ K' for every candidate K'), which is false in general (incomparable minimal complements);
3. the interface forces 1 < |Φ(K)|, but the manuscript explicitly allows R = Φ(K) = 1 (thm:closedrecursion: "when R ≠ 1"; the inductive step l.4542: "If R = 1, then B = Y and the induction closes at this [elementary] stage").

This file is the corrected, PROVEN foundation:

• FirstNonScalarChiefFactor — a non-scalar chief factor all of whose strictly-below chief factors are scalar; firstNonScalarChiefFactor_exists (choose a non-scalar chief factor of least upper cardinality) is proved, from ¬ ScalarTerminal p alone.
• KernelMinimal — the manuscript's kernel: K ◁ Y, K ≤ P, KS = P, and ⊆-minimality inside K (exactly the form used by lem:simplehead and lem:collapse); kernelMinimal_exists is proved by finite descent.
• frattini_case_split — the R = 1 / R ≠ 1 dichotomy of thm:closedrecursion, stated on the literal Φ(K) ≤ Y.

No axioms are introduced here; everything is proved.

Cardinality helpers for subgroups of the finite target

theorem Q2Presentation.Induction.subgroup_card_lt_of_lt {p : FramedPair} {H K : Subgroup p.fst.Y} (h : H < K) : Nat.card ↥H < Nat.card ↥K

Strict monotonicity of Nat.card on subgroups of the finite target group.

The first non-scalar chief factor

structure Q2Presentation.Induction.FirstNonScalarChiefFactor (p : FramedPair) extends Q2Presentation.Induction.NonScalarChiefFactor p : Type

A non-scalar chief factor of L_Y that is first: every chief factor strictly below it (i.e. with upper term contained in lower) is scalar. This is the manuscript's choice S ◁ P at l.3616–3623 ("all chief factors below S are scalar and V is the first non-scalar simple factor"), which lem:collapse requires for the coprime step [S, Ñ] = 1.

• lower : Subgroup p.fst.Y
• upper : Subgroup p.fst.Y
• chief : ChiefFactorInLY p.fst self.lower self.upper
• nontrivial_action : ¬ChiefFactorTrivial p.fst self.lower self.upper
• below_scalar (M N : Subgroup p.fst.Y) : ChiefFactorInLY p.fst M N → N ≤ self.lower → ChiefFactorTrivial p.fst M N

theorem Q2Presentation.Induction.firstNonScalarChiefFactor_exists {p : FramedPair} (h : ¬ScalarTerminal p) : Nonempty (FirstNonScalarChiefFactor p)

Existence of a first non-scalar chief factor (proved, no axioms): among all non-scalar chief factors pick one whose upper term has least cardinality; anything strictly below it is smaller, hence scalar by minimality.

The manuscript's ⊆-minimal kernel

structure Q2Presentation.Induction.KernelMinimal {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

The manuscript's kernel choice (l.3623): K ◁ Y, K ≤ P, KS = P, and K is ⊆-minimal with these properties — stated as: any Y-normal K' ≤ K still joining with S to P equals K. (This, not leastness among all candidates, is what lem:simplehead and lem:collapse use: both apply it to subgroups of K.)

• Ksub : Subgroup p.fst.Y
• Ksub_normal : self.Ksub.Normal
• Ksub_le_upper : self.Ksub ≤ chief.upper
• KS_eq_upper : self.Ksub ⊔ chief.lower = chief.upper
• minimal_inside (K' : Subgroup p.fst.Y) : K'.Normal → K' ≤ self.Ksub → K' ⊔ chief.lower = chief.upper → K' = self.Ksub

theorem Q2Presentation.Induction.KernelMinimal.Ksub_le_LY {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : K.Ksub ≤ p.fst.LY

K ≤ L_Y (the wild kernel), via K ≤ P ≤ L_Y.

theorem Q2Presentation.Induction.kernelMinimal_exists {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelMinimal chief)

Existence of a ⊆-minimal kernel (proved, no axioms): finite descent on Nat.card K starting from the candidate K = P itself.

The R = Φ(K) case split (thm:closedrecursion)

def Q2Presentation.Induction.kernelFrattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Subgroup p.fst.Y

The literal Frattini subgroup R = Φ(K) of the kernel, as a subgroup of Y (the manuscript's R, l.3626).

Equations

• Q2Presentation.Induction.kernelFrattini K = Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub)

theorem Q2Presentation.Induction.frattini_case_split {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Nat.card ↥(kernelFrattini K) = 1 ∨ 1 < Nat.card ↥(kernelFrattini K)

The R = 1 / R ≠ 1 dichotomy of thm:closedrecursion (l.4429/4437): either the Frattini layer is trivial — "B = Y and the induction closes at the elementary stage" — or it is a genuine strict layer and the R-obstruction stages apply.