Route141 Section 7 kernel raw closers

This attack sidecar leaves the public route and all existing Route43/Route138 files untouched. It targets the Route141 kernel raw frontier:

• the Route43 literal R, M, T, C raw-object/action atoms;
• the monolithic same-tower invariant packet minimalBlock_invariantActualProofs2Data.

The literal Route43 structures are reassembled from Route141-owned lower field packets. The invariant packet is rebuilt through MinimalBlockInvariantActualProofs3, so the old invariant axiom is not in the new integrated theorem closure.

Route141-owned literal raw object/equivalence packets

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

• toObject : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F

structure Q2Presentation.Induction.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.RawQuotientLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

• toObject : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F

structure Q2Presentation.Induction.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.RawLowerLiteralQuotientObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

• toObject : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F

structure Q2Presentation.Induction.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.rawFrattiniLiteralObjectCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawFrattiniLiteralObjectCoreData K F)

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

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

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

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

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

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

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.frattiniLiteralModuleObject_from_route141RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelConcreteRoute43.RawFrattiniLiteralModuleObjectData K F)

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.quotientLiteralModuleObject_from_route141RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelConcreteRoute43.RawQuotientLiteralModuleObjectData K F)

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.submoduleLiteralObject_from_route141RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Nonempty (MinimalBlockKernelConcreteRoute43.RawSubmoduleLiteralObjectData Mobj)

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.lowerLiteralQuotientGroup_from_route141RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelConcreteRoute43.RawLowerLiteralQuotientGroupData K F)

Route141-owned raw action packets

structure Q2Presentation.Induction.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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.Section7KernelRoute141RawClosers.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

• ⋯ = ⋯

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.frattiniTransportAction_from_route141RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData Robj Cobj)

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.moduleTransportAction_from_route141RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData Mobj Cobj)

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.submoduleTransportStable_from_route141RawClosers {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 (MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData Tobj A.toRoute43)

Raw quotient tower and invariant replacements

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

Route141 same-raw-tower simple-head action packet used only to install the nonzero quotient head in the raw quotient tower. The invariant theorem below handles dual-vanishing and the lower scalar character separately.

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.rawObjectActionBridgeData_from_route141RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData K F)

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

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.minimalBlock_invariantActualProofs2Data_from_section7KernelRoute141RawClosers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Route141 kernel provider with raw/invariant atoms swapped

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute141RawClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute141RawClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

theorem Q2Presentation.Induction.Section7KernelRoute141RawClosers.minimalBlock_groupTowerData_from_section7KernelRoute141RawClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Integrated theorem with the Route141 raw/invariant kernel provider

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

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

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