Route39 minimal-block kernel/head refinement #

This sidecar is intentionally standalone: no routed or root files import it yet.

Route38 exposes the Section 7 kernel/head frontier through split concrete packets plus four Route38 raw-head packets. Route39 exports a drop-in group tower provider whose axiom closure avoids those Route38 names. The replacement frontier is:

the route26 upper-candidate leastness packet for the selected K;
one manuscript lem:collapse packet for the literal Phi(K), with normality proved from characteristicity and nontriviality lowered to a nonidentity witness;
the finer raw quotient transport packets for R, M, T, C, the induced actions, T-stability, the literal K/Phi(K) ~= M bridge, and a nonzero head coset;
the existing same-raw-tower simple-head/scalar actual closer.

Route39 Frattini-centralizer collapse packet #

source

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.FrattiniCentralizerCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Prop

Route39 residual for the hard finite-group content of manuscript lem:collapse, attached to the already selected least kernel K.

Normality of Phi(K) in Y is theorem-level from K.Normal, so this packet only keeps the nonidentity witness and the pointwise collapse conclusions: centrality in K, K^4 = 1, and exponent two on Phi(K).

frattini_nonidentity : ∃ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), r ≠ 1
frattini_central_in_K (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → ∀ k ∈ K.Ksub, r * k = k * r
K_fourth_eq_one (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1
frattini_square_eq_one (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → r ^ 2 = 1

Instances For

source

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.frattiniCentralizerCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (FrattiniCentralizerCollapseData K)

Route39 residual: the Frattini-centralizer collapse for the selected K.

This is the remaining finite group argument from lem:collapse: Hall/coprime action gives centrality of Phi(K), fourth powers vanish on K, and the Frattini layer is elementary abelian.

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.frattiniNormalData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

MinimalBlockKernelModuleConcreteFrattiniNormalData K

Normality of the literal Frattini subgroup is closed theorem-level from normality of the selected K.

Equations

⋯ = ⋯

Instances For

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.frattiniNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCollapseData K) :

MinimalBlockKernelModuleConcreteFrattiniNontrivialData K

The Route39 nonidentity witness gives the existing cardinal nontriviality packet.

Equations

⋯ = ⋯

Instances For

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.frattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCollapseData K) :

MinimalBlockKernelModuleConcreteFrattiniData K

The Route39 collapse packet reassembles the current concrete Frattini data.

Equations

⋯ = ⋯

Instances For

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.frattiniData_from_route39Collapse {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Route-ready Frattini data through the Route39 collapse packet.

Raw quotient transport through finer packets #

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.rawQuotientTowerData_from_route39Transport {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Raw quotient tower assembled from the existing finer object/action/bridge/head transport packets, avoiding the Route38 raw-object and raw-action aggregate residual names.

Concrete provenance and group tower #

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute39.kernelModuleConcreteProvenanceData_from_route39 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete provenance through the Route39 least/collapse/transport route.

This is the Route38 concrete provenance assembly with the Route38-listed kernel/head residual names replaced by Route39's collapse packet and the finer quotient transport packets.

source