Route164 Section 7 kernel/provenance closers

This sidecar leaves Route163 and Route161 untouched. It supplies a drop-in kernel provider for the Route163 Fourier branch, but routes the Section 7 kernel/provenance work through Route164-owned lower atoms:

• least K is split into a selected candidate and a universal leastness field;
• the Frattini collapse is split into normality proved from K.Normal, nonidentity, centralizer-step, fourth-power, and elementary-layer fields;
• the Route43 literal raw object/action wrappers are split into object, equivalence, action-family, and pointwise-stability packets;
• the Route43 simple-head atoms are replaced by the direct Route44 semantic head fields on the same raw tower.

The replayed finite-count theorem below swaps only the kernel provider used by Route163.

Least kernel and Frattini collapse

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

Route164 selected candidate for the minimal normal K <= P with K S = P.

• 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

structure Q2Presentation.Induction.Section7KernelRoute164Closers.LeastUniversalData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : LeastCandidateData chief) : Prop

Route164 universal leastness for the selected candidate.

• minimal_K (K' : Subgroup p.fst.Y) : K'.Normal → K' ≤ chief.upper → K' ⊔ chief.lower = chief.upper → K.Ksub ≤ K'

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.leastCandidateData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (LeastCandidateData chief)

Residual selected candidate for the Section 7 least kernel.

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.leastUniversalData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : LeastCandidateData chief) : Nonempty (LeastUniversalData K)

Residual universal leastness for the Route164 selected candidate.

def Q2Presentation.Induction.Section7KernelRoute164Closers.leastOverChiefDataOfRoute164 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : LeastCandidateData chief) (L : LeastUniversalData K) : MinimalBlockKernelLeastOverChiefData chief

Assemble the current least-over-chief interface from the Route164 split.

Equations

• Q2Presentation.Induction.Section7KernelRoute164Closers.leastOverChiefDataOfRoute164 K L = { Ksub := K.Ksub, Ksub_normal := ⋯, Ksub_le_upper := ⋯, KS_eq_upper := ⋯, minimal_K := ⋯ }

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.leastOverChiefData_from_route164 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route164 replacement for minimalBlock_kernelLeastOverChiefData.

structure Q2Presentation.Induction.Section7KernelRoute164Closers.FrattiniNonidentityData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Witness-form nontriviality of the literal Frattini layer.

• exists_nonidentity : ∃ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), r ≠ 1

structure Q2Presentation.Induction.Section7KernelRoute164Closers.FrattiniCentralizerStepData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Centralizer-step form of the Frattini-centralizer collapse.

• K_centralizes_frattini (k : p.fst.Y) : k ∈ K.Ksub → ∀ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), k * r = r * k

structure Q2Presentation.Induction.Section7KernelRoute164Closers.FourthPowerMapVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Fourth-power-map vanishing in Lemma 7.2.

• fourth_power_vanishes (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1

structure Q2Presentation.Induction.Section7KernelRoute164Closers.FrattiniElementaryLayerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Elementary Frattini-layer conclusion in Lemma 7.2.

• frattini_square_eq_one (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → r ^ 2 = 1

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniNonidentityData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniNonidentityData K)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniCentralizerStepData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerStepData K)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.fourthPowerMapVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerMapVanishesData K)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniElementaryLayerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniElementaryLayerData K)

def Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniNormalData_from_route164 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : MinimalBlockKernelModuleConcreteFrattiniNormalData K

Normality of the literal Frattini subgroup is theorem-level from K.Normal.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniNontrivialDataOfNonidentity {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (W : FrattiniNonidentityData K) : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K

Convert a nonidentity Frattini element to cardinal nontriviality.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniNontrivialData_from_route164 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNontrivialData K)

Route164 replacement for Frattini nontriviality.

def Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniCentralDataOfCentralizerStep {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerStepData K) : MinimalBlockKernelModuleConcreteFrattiniCentralData K

Route164 replacement for Frattini centrality.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute164Closers.fourthPowerDataOfMapVanishes {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerMapVanishesData K) : MinimalBlockKernelModuleConcreteFourthPowerData K

Route164 replacement for fourth-power vanishing.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniExponentDataOfElementaryLayer {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniElementaryLayerData K) : MinimalBlockKernelModuleConcreteFrattiniExponentData K

Route164 replacement for exponent two on the Frattini layer.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.frattiniData_from_route164 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Route164 Frattini-collapse packet for the selected least kernel.

Raw literal objects and transported actions

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawFrattiniLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

• toObject : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawFrattiniLiteralEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) : Type

• frattini_equiv_rawR : ↥(Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub)) ≃* Multiplicative Robj.R

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawQuotientLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

• toObject : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawQuotientLiteralEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Type

• KmodR_equiv_rawM : ↥(Subgroup.map (QuotientGroup.mk' (Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub))) K.Ksub) ≃* Multiplicative Mobj.M

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawSubmoduleLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Type

• toObject : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawLowerLiteralQuotientObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

• toObject : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawLowerLiteralQuotientEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Type

• quotient_equiv_C : p.fst.Y ⧸ K.Ksub ≃* Cobj.C

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawFrattiniLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawFrattiniLiteralObjectCoreData K F)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawFrattiniLiteralEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) : Nonempty (RawFrattiniLiteralEquivData Robj)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawQuotientLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawQuotientLiteralObjectCoreData K F)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawQuotientLiteralEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Nonempty (RawQuotientLiteralEquivData Mobj)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawSubmoduleLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Nonempty (RawSubmoduleLiteralObjectCoreData Mobj)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawLowerLiteralQuotientObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawLowerLiteralQuotientObjectCoreData K F)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawLowerLiteralQuotientEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (RawLowerLiteralQuotientEquivData Cobj)

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawFrattiniTransportActionFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Type

• actR : Cobj.C → Robj.R ≃ₗ[ZMod 2] Robj.R
• actR_one : self.actR 1 = 1
• actR_mul (c d : Cobj.C) : self.actR (c * d) = self.actR c * self.actR d

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawModuleTransportActionFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Type

• actM : Cobj.C → Mobj.M ≃ₗ[ZMod 2] Mobj.M
• actM_one : self.actM 1 = 1
• actM_mul (c d : Cobj.C) : self.actM (c * d) = self.actM c * self.actM d

structure Q2Presentation.Induction.Section7KernelRoute164Closers.RawSubmodulePointwiseStableData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (A : RawModuleTransportActionFamilyData Mobj Cobj) : Prop

• T_stable (c : Cobj.C) (m : Mobj.M) : m ∈ Tobj.T → (A.actM c) m ∈ Tobj.T

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawFrattiniTransportActionFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (RawFrattiniTransportActionFamilyData Robj Cobj)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawModuleTransportActionFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (RawModuleTransportActionFamilyData Mobj Cobj)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawSubmodulePointwiseStableData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (A : RawModuleTransportActionFamilyData Mobj Cobj) : Nonempty (RawSubmodulePointwiseStableData Tobj A)

def Q2Presentation.Induction.Section7KernelRoute164Closers.RawFrattiniTransportActionFamilyData.toRoute43 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (A : RawFrattiniTransportActionFamilyData Robj Cobj) : MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData Robj Cobj

Equations

• A.toRoute43 = { actR := { toFun := A.actR, map_one' := ⋯, map_mul' := ⋯ } }

def Q2Presentation.Induction.Section7KernelRoute164Closers.RawModuleTransportActionFamilyData.toRoute43 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (A : RawModuleTransportActionFamilyData Mobj Cobj) : MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData Mobj Cobj

Equations

• A.toRoute43 = { actM := { toFun := A.actM, map_one' := ⋯, map_mul' := ⋯ } }

def Q2Presentation.Induction.Section7KernelRoute164Closers.RawSubmodulePointwiseStableData.toRoute43 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} {Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj} {A : RawModuleTransportActionFamilyData Mobj Cobj} (S : RawSubmodulePointwiseStableData Tobj A) : MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData Tobj A.toRoute43

Equations

• ⋯ = ⋯

Same-tower simple head fields

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawInvariantHyperplanesContainTData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawHeadNonzeroStableEqTopData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadNonzeroStableEqTopData D)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawHeadActionNotPointwiseTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

axiom Q2Presentation.Induction.Section7KernelRoute164Closers.rawLowerInvariantCharacterExistsData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.rawSimpleHeadSemanticData_from_route164 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route164 direct simple-head semantic packet for the selected raw tower.

Route164 kernel provider

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.rawQuotientTowerData_from_route164 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Raw quotient tower assembled from Route164 literal objects/actions and same-tower simple-head fields.

def Q2Presentation.Induction.Section7KernelRoute164Closers.concreteProvenanceDataOfRawQuotientTower {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) (Q : MinimalBlockKernelRawQuotientTowerData K F) : MinimalBlockKernelModuleConcreteProvenanceData chief

Assemble concrete provenance from a Route164 raw quotient tower.

Equations

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

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute164Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route164 lower atoms.

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute164Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route164.

theorem Q2Presentation.Induction.Section7KernelRoute164Closers.minimalBlock_groupTowerData_from_section7KernelRoute164Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in Route164 replacement for Section7KernelRoute161Closers.minimalBlock_groupTowerData_from_section7KernelRoute161Closers.

Route163 replay with the Route164 kernel provider

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated164KernelRoute164 (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated164KernelRoute164 (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated164KernelRoute164 (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_currentIntegrated164KernelRoute164 (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated164KernelRoute164 (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Finite-surjection equality for Route163 with the Route164 kernel lowering.