Documentation

Q2Presentation.Induction.Section7KernelRoute143RawActualClosers

Route143 Section 7 raw actual closers #

This route-neutral sidecar leaves the current Route143 integrated file untouched. It targets the raw Section 7 kernel atoms exposed there by replacing the Route141 raw object/action split with three same-tower manuscript packets:

the literal object tower R = Phi(K), M = K/Phi(K), T, and C = Y/K;
the transported actions on that same tower;
the simple-head/lower-character packet on the resulting raw tower.

The route-ready providers below avoid the Route141 namespace-local raw atoms and avoid the three broad raw-head/lower-scalar atoms in the invariant packet.

Same-tower raw object/action packets #

structure Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.RawLiteralObjectTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Route143 literal object tower for the Section 7 raw extraction.

The four fields are selected together so later action and bridge data cannot mix unrelated choices of R, M, T, and C.

Rlit : MinimalBlockKernelConcreteRoute43.RawFrattiniLiteralModuleObjectData K F
Mlit : MinimalBlockKernelConcreteRoute43.RawQuotientLiteralModuleObjectData K F
Tlit : MinimalBlockKernelConcreteRoute43.RawSubmoduleLiteralObjectData self.Mlit.toObject
Clit : MinimalBlockKernelConcreteRoute43.RawLowerLiteralQuotientGroupData K F

Instances For

structure Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.RawLiteralTransportActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : RawLiteralObjectTowerData K F) :

Route143 transported action packet over one selected literal object tower.

actR : MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData O.Rlit.toObject O.Clit.toObject
actM : MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData O.Mlit.toObject O.Clit.toObject
stable : MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData O.Tlit.toObject self.actM

Instances For

structure Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.RawSimpleHeadActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Route143 raw simple-head packet on one selected raw tower.

invariantHyperplanes : MinimalBlockRawInvariantHyperplanesContainTData D
headNonzeroStable : MinimalBlockRawHeadNonzeroStableEqTopData D
headActionNotPointwiseTrivial : MinimalBlockRawHeadActionNotPointwiseTrivialData D
lowerInvariantCharacter : MinimalBlockRawLowerInvariantCharacterExistsData D

Instances For

axiom Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.rawLiteralObjectTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Nonempty (RawLiteralObjectTowerData K F)

Residual literal object tower packet for Route143.

axiom Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.rawLiteralTransportActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : RawLiteralObjectTowerData K F) :

Nonempty (RawLiteralTransportActionData O)

Residual transported action packet over the selected literal object tower.

axiom Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.rawSimpleHeadActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (RawSimpleHeadActualData D)

Residual simple-head/lower-character packet over the selected raw tower.

def Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.RawSimpleHeadActualData.toRoute44 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : RawSimpleHeadActualData D) :

MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D

Equations

⋯ = ⋯

Instances For

Raw quotient tower #

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

Nonempty (MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData K F)

Route78-shaped raw object/action/bridge data from the Route143 same-tower literal object and transport packets.

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

Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Replacement for the Route141 raw quotient tower provider.

This theorem does not use the eleven Route141 raw object/action atoms. It uses the Route143 literal object tower, transported action tower, and same-raw-tower simple-head packet instead.

Raw-head and invariant actual packet #

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.rawSimpleHeadSemanticData_from_section7KernelRoute143RawActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.minimalBlock_rawHeadQuotientNoTrivialData_from_section7KernelRoute143RawActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadQuotientNoTrivialData D)

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.minimalBlock_rawHeadSimplicityActualData_from_section7KernelRoute143RawActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadSimplicityActualData D)

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.minimalBlock_rawLowerScalarQuotientData_from_section7KernelRoute143RawActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawLowerScalarQuotientData D)

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.minimalBlock_invariantActualProofs2Data_from_section7KernelRoute143RawActualClosers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :

Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Replacement for Section7KernelRoute141RawClosers.minimalBlock_invariantActualProofs2Data_from_section7KernelRoute141RawClosers_lower.

Route143 kernel provider #

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute143RawActualClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute143RawActualClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockLowerGroupModuleData chief)

theorem Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.minimalBlock_groupTowerData_from_section7KernelRoute143RawActualClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Route143 audit branch using the Route143 raw actual kernel provider #

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

¬ScalarTerminal p → Nonempty (FourierBranchData p)

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

framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated143RawActualLowered (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)))