Section 7 Frattini centrality, exported to the concrete kernel packets

The corrected Section 7 trunk proves

kernel_commutator_frattini_eq_bot : ⁅K.Ksub, kernelFrattini K⁆ = ⊥

for the manuscript kernel K : KernelMinimal chief.toNonScalarChiefFactor attached to a first non-scalar chief factor. This sidecar pushes that theorem back through the older MinimalBlockKernelModuleConcreteFrattiniData interfaces:

• first, a least-over-chief kernel packet is converted to the corrected KernelMinimal packet. This conversion is theorem-level: the old leastness field is stronger than the corrected minimal_inside field, so no new axiom is needed;
• then the commutator equality is converted to the elementwise field frattini_central_in_K;
• finally, the remaining Frattini-collapse packet is split so that the exponent-two field is obtained from the new centrality theorem plus the already-isolated fourth-power and square/commutator-layer inputs. Thus a direct closure of K_fourth_eq_one is left as the next independent manuscript lemma, rather than being entangled with centrality.

This file is route-neutral: it introduces no axioms and does not edit existing routed files. It is intended to be imported by the next root route when replacing the old minimalBlock_kernelModuleConcreteFrattiniCentralData residual.

def Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalOfLeastOverChief {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) : KernelMinimal chief.toNonScalarChiefFactor

Convert the older least-over-chief kernel packet to the corrected manuscript KernelMinimal packet. The old minimal_K field is stronger than what the corrected interface needs: applying it to a candidate K' ≤ K gives K ≤ K', and hence equality.

Equations

• Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalOfLeastOverChief chief K = { Ksub := K.Ksub, Ksub_normal := ⋯, Ksub_le_upper := ⋯, KS_eq_upper := ⋯, minimal_inside := ⋯ }

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelFrattini_central_in_K {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (r : p.fst.Y) : r ∈ kernelFrattini K → ∀ k ∈ K.Ksub, r * k = k * r

Elementwise centrality form of kernel_commutator_frattini_eq_bot for the corrected KernelMinimal interface.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.leastOverChief_frattini_central_in_K {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → ∀ k ∈ K.Ksub, r * k = k * r

Elementwise centrality for the older least-over-chief packet, obtained by transporting through kernelMinimalOfLeastOverChief. This is the direct replacement for the field frattini_central_in_K.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniCentralData_from_kernel_commutator_frattini_eq_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniCentralData K)

Concrete MinimalBlockKernelModuleConcreteFrattiniCentralData, closed from the new commutator theorem. This avoids the old residual minimalBlock_kernelModuleConcreteFrattiniCentralData whenever the chief factor is the first non-scalar one used in the corrected Section 7 route.

def Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniCentralizerStepData_from_kernel_commutator_frattini_eq_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K

Route60 centralizer-step shape, also closed from the new commutator theorem. The Route60 step is in the opposite orientation (k * r = r * k), so this is just the symmetric form of leastOverChief_frattini_central_in_K.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniCentralData_from_route60Step_kernel_commutator {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniCentralData K)

The concrete centrality packet can equivalently be recovered through the existing Route60 adapter. This theorem is useful for route files that already consume a FrattiniCentralizerStepData rather than the final field packet.

Remaining Frattini-collapse split after centrality

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniExponentData_from_kernel_commutator_fourthPower_squareCommutator {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (P4 : MinimalBlockKernelModuleConcreteFourthPowerData K) (E : MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Exponent-two on the literal Frattini layer, after centrality has been closed.

The remaining inputs are exactly the two manuscript mechanisms that are independent of centrality:

• P4: the fourth-power vanishing map on K;
• E: the square/commutator-layer form of Φ(K) = K²[K,K].

This theorem removes any need to assume a separate centralizer-collapse packet in order to obtain the old MinimalBlockKernelModuleConcreteFrattiniExponentData field.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniData_from_kernel_commutator_fourthPower_squareCommutator {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (N : MinimalBlockKernelModuleConcreteFrattiniNormalData K) (C : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K) (P4 : MinimalBlockKernelModuleConcreteFourthPowerData K) (E : MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

A route-ready assembly theorem for the concrete Frattini packet after centrality.

Compared with MinimalBlockKernelModuleConcreteFrattiniData.ofSplit, this version no longer requires the old centrality residual and no longer requires an independent exponent residual. The remaining Frattini-collapse inputs are:

• normality of the literal Frattini subgroup;
• nontriviality of the literal Frattini subgroup in the R ≠ 1 branch;
• fourth-power vanishing on K;
• the square/commutator-layer generation/exponent packet.

structure Q2Presentation.Induction.Section7FrattiniCentralConcrete.KernelMinimalFourthPowerCandidateData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

The strict next theorem-level split for the fourth-power field over the corrected kernel interface. To close K_fourth_eq_one, it is enough to produce a normal subgroup inside K, still mapping onto the selected chief factor, on which fourth powers vanish. This is the corrected minimal-inside version of the older Route63/Route67 fourth-power-kernel candidate.

• fourthKernel : Subgroup p.fst.Y
• fourthKernel_normal : self.fourthKernel.Normal
• fourthKernel_le_K : self.fourthKernel ≤ K.Ksub
• fourthKernel_sup_lower : self.fourthKernel ⊔ chief.lower = chief.upper
• fourthKernel_fourth_eq_one (k : p.fst.Y) : k ∈ self.fourthKernel → k ^ 4 = 1

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimal_K_fourth_eq_one_of_fourthPowerCandidate {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerCandidateData chief K) (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1

Fourth-power vanishing from the corrected fourth-power-kernel candidate.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.fourthPowerData_from_kernelMinimalFourthPowerCandidate {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerCandidateData chief (kernelMinimalOfLeastOverChief chief K)) : Nonempty (MinimalBlockKernelModuleConcreteFourthPowerData K)

Old concrete fourth-power packet from the corrected fourth-power-kernel candidate, for routes that still use MinimalBlockKernelLeastOverChiefData.