Route172 Section 7 kernel/raw closers

This sidecar leaves all integrated route files untouched. It supplies the same group-tower target as Section7KernelRoute169Closers.minimalBlock_groupTowerData_from_section7KernelRoute169Closers, but replaces the Route169/Route146 raw-head split by the coherent Route143 same-raw-tower actual packet:

• selected least K and R = Phi(K) still come from the current Route141 Frattini path;
• the raw R, M = K/R, T, C object/action bridge is selected by the Route143 raw-actual tower packet;
• the simple-head/lower-character facts are selected together on that raw tower, so the provider does not call the standalone raw-head/lower-scalar atoms or the Route141 raw object/action atoms.

Coherent raw-actual kernel packet

structure Q2Presentation.Induction.Section7KernelRoute172Closers.KernelRoute172RawActualLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route172 same-tower kernel/raw packet.

The Frattini part intentionally stays on the current Route141 frontier. The raw part is lowered from the Route141 raw split and the four standalone raw-head atoms to the Route143 coherent raw-object/action and simple-head packets.

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

def Q2Presentation.Induction.Section7KernelRoute172Closers.KernelRoute172RawActualLayerData.rawSimpleSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute172RawActualLayerData chief) : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D.rawBridge.rawData.rawTowerData

The Route44 semantic simple-head packet carried by the Route172 raw-actual data.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute172Closers.KernelRoute172RawActualLayerData.rawQuotientTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute172RawActualLayerData chief) : MinimalBlockKernelRawQuotientTowerData D.least ⋯

The raw quotient/head packet recovered from the coherent Route172 data.

Equations

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

def Q2Presentation.Induction.Section7KernelRoute172Closers.KernelRoute172RawActualLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute172RawActualLayerData chief) : MinimalBlockKernelModuleConcreteProvenanceData chief

Forget the Route172 raw-actual packet to concrete kernel provenance.

Equations

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

def Q2Presentation.Induction.Section7KernelRoute172Closers.KernelRoute172RawActualLayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute172RawActualLayerData chief) : MinimalBlockLowerGroupModuleData chief

The lower group/module tower selected by the Route172 packet.

Equations

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

def Q2Presentation.Induction.Section7KernelRoute172Closers.KernelRoute172RawActualLayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute172RawActualLayerData chief) : MinimalBlockInvariantActualProofs2Data D.lowerGroupModuleData.rawTowerData

The actual invariant packet obtained from the same raw-simple fields.

Equations

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

def Q2Presentation.Induction.Section7KernelRoute172Closers.KernelRoute172RawActualLayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute172RawActualLayerData chief) : MinimalBlockGroupTowerData p chief

The group tower consumed by the Fourier branch.

Equations

• D.groupTowerData = D.lowerGroupModuleData.groupTowerData ⋯ ⋯

Route169-compatible providers

theorem Q2Presentation.Induction.Section7KernelRoute172Closers.kernelRoute172RawActualLayerData_from_section7KernelRoute172Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute172RawActualLayerData chief)

Route172 raw-actual module-layer packet from the current Route141 Frattini path and the Route143 raw-actual tower.

theorem Q2Presentation.Induction.Section7KernelRoute172Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute172Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route172.

theorem Q2Presentation.Induction.Section7KernelRoute172Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute172Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route172.

theorem Q2Presentation.Induction.Section7KernelRoute172Closers.minimalBlock_groupTowerData_from_section7KernelRoute172Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in Route172 replacement for Section7KernelRoute169Closers.minimalBlock_groupTowerData_from_section7KernelRoute169Closers.

Route171 replay with only the kernel provider lowered

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

Route171 nonterminal Fourier branch with only the Section 7 kernel provider swapped to Route172.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated172KernelRoute172 (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_currentIntegrated172KernelRoute172 (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_currentIntegrated172KernelRoute172 (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated172KernelRoute172 (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 Route171 with only the Section 7 kernel provider replaced by Route172.