Documentation

Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers

Route175 Section 7 kernel Frattini carrier closer #

This route-neutral sidecar leaves the integrated Route174 files untouched. It replays the Route174 kernel provider, but closes one of the Route141 Frattini selector atoms theorem-level:

the generated-layer carrier is chosen to be the literal embedded Phi(K) = Subgroup.map K.Ksub.subtype (frattini K.Ksub);
the remaining exponent-transfer obligation stays exposed as the existing Route141 frattiniGeneratedLayerCarrierExponentData atom.

This is a strict lowering of the expanded Route174 kernel frontier: the provider no longer depends on Section7KernelRoute141FrattiniClosers.frattiniGeneratedLayerCarrierData.

Literal generated-layer carrier #

def Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.literalGeneratedLayerCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Section7KernelRoute141FrattiniClosers.FrattiniGeneratedLayerCarrierData K

Route175 closes the generated-layer carrier selector by taking the carrier to be the literal embedded Frattini subgroup itself.

Equations

Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.literalGeneratedLayerCarrierData K = { carrier := Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), frattini_le_carrier := ⋯ }

Instances For

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.frattiniGeneratedLayerCarrierData_from_route175Literal {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (Section7KernelRoute141FrattiniClosers.FrattiniGeneratedLayerCarrierData K)

The Route141 generated-layer carrier atom is theorem-level for the literal carrier used in Route175.

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.frattiniGeneratedLayerExponentData_from_route175Literal {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute81Closers.FrattiniGeneratedLayerExponentData K)

Route81-shaped generated-layer exponent packet using the literal Route175 carrier. This keeps the actual exponent-transfer assumption visible and drops only the carrier-selection atom.

Route141 Frattini replay with the carrier selector closed #

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.frattiniSquareCommutatorLiteralExponentData_from_route175Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K)

Route78 literal exponent packet through Route175's literal carrier.

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.frattiniSquareCommutatorLayerData_from_route175Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K)

Route67 square/commutator layer packet through Route175.

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.frattiniElementaryLayerData_from_route175Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniElementaryLayerData K)

Elementary Frattini layer through Route175.

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.frattiniExponentData_from_route175Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Concrete exponent-two packet through Route175.

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.frattiniData_from_route175Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet with the generated-layer carrier closed theorem-level.

Route172-shaped raw actual kernel packet #

structure Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) :

Route175 same-tower kernel/raw packet. It is Route172's packet with the Frattini concrete packet rebuilt through the literal carrier closure above.

least : MinimalBlockKernelLeastOverChiefData chief
frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
rawBridge : MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData self.least ⋯
rawSimple : Section7KernelRoute143RawActualClosers.RawSimpleHeadActualData self.rawBridge.rawData.rawTowerData

Instances For

def Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData.rawSimpleSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute175RawActualLayerData chief) :

MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D.rawBridge.rawData.rawTowerData

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData.rawQuotientTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute175RawActualLayerData chief) :

MinimalBlockKernelRawQuotientTowerData D.least ⋯

Equations

D.rawQuotientTowerData = { objects := D.rawBridge.rawObjects, actions := D.rawBridge.rawActions, bridge := id (id D.rawBridge.rawBridge), head := ⋯ }

Instances For

def Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute175RawActualLayerData chief) :

MinimalBlockKernelModuleConcreteProvenanceData chief

Equations

D.concreteProvenanceData = Q2Presentation.Induction.Section7KernelRoute169Closers.concreteProvenanceDataOfRawQuotientTower D.least ⋯ D.rawQuotientTowerData

Instances For

def Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute175RawActualLayerData chief) :

MinimalBlockLowerGroupModuleData chief

Equations

D.lowerGroupModuleData = Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance D.concreteProvenanceData

Instances For

def Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute175RawActualLayerData chief) :

MinimalBlockInvariantActualProofs2Data D.lowerGroupModuleData.rawTowerData

Equations

D.invariantActualData = id (Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_of_rawSimpleHeadSemanticData ⋯)

Instances For

def Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute175RawActualLayerData chief) :

MinimalBlockGroupTowerData p chief

Equations

D.groupTowerData = D.lowerGroupModuleData.groupTowerData ⋯ ⋯

Instances For

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.kernelRoute175RawActualLayerData_from_section7KernelRoute175FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (KernelRoute175RawActualLayerData chief)

Route175 raw-actual module-layer packet from Route141 Frattini data with the carrier atom closed and the Route143 same-raw-tower actual packet.

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute175FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute175FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockLowerGroupModuleData chief)

theorem Q2Presentation.Induction.Section7KernelRoute175FrattiniClosers.minimalBlock_groupTowerData_from_section7KernelRoute175FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in Route175 replacement for Section7KernelRoute172Closers.minimalBlock_groupTowerData_from_section7KernelRoute172Closers.

Route174 replay with only the kernel provider lowered #

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated175KernelRoute175 (p : FramedPair) :

¬ScalarTerminal p → Nonempty (FourierBranchData p)

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated175KernelRoute175 (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_currentIntegrated175KernelRoute175 (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_currentIntegrated175KernelRoute175 (p : FramedPair) :

framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated175KernelRoute175 (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 Route174 with the Route175 kernel provider.