Route157 Section 7 kernel/provenance closers

This sidecar leaves the integrated route files untouched. It lowers the Route156 kernel/provenance frontier by rebuilding the Route152 kernel bridge from two manuscript-shaped packets already present in the tree:

• the Route141 Frattini split for the selected least K and R = Phi(K) collapse, replacing the five Route78 selected atoms;
• the Route143 same-tower raw object/action and simple-head packets, replacing the Route141 raw object/action atoms and the three independent raw invariant facts on the selected raw tower.

The bridge targets KernelRoute152ProvenanceModuleFacts, then uses Route152's axiom-free bridge to the Route151 package shape consumed by the current kernel route. The replayed finite-count theorem below does not call Section7KernelRoute151Closers.kernelRoute151SelectedPackageData.

Coherent Route157 kernel packet

structure Q2Presentation.Induction.Section7KernelRoute157Closers.KernelRoute157RawActualFrattiniFacts {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route157 same-tower kernel/provenance packet.

The Frattini part is selected by the Route141 Frattini split. The raw tower and head/lower-character facts are selected by the Route143 raw-actual packet, so the object/action bridge and invariant fields all refer to the same R, M, T, C tower.

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

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

The Route44 semantic simple-head packet carried by the Route157 data.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute157Closers.KernelRoute157RawActualFrattiniFacts.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute157RawActualFrattiniFacts chief) : MinimalBlockInvariantActualProofs2Data D.rawBridge.rawData.rawTowerData

Reassemble the actual invariant packet from the Route143 raw-simple data.

Equations

• D.invariantActualData = Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_of_rawSimpleHeadSemanticData ⋯

def Q2Presentation.Induction.Section7KernelRoute157Closers.KernelRoute157RawActualFrattiniFacts.headActionData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute157RawActualFrattiniFacts chief) : MinimalBlockRawHeadActionNotPointwiseTrivialData D.rawBridge.rawData.rawTowerData

The same raw tower's head action is not pointwise trivial.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute157Closers.KernelRoute157RawActualFrattiniFacts.dualInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute157RawActualFrattiniFacts chief) : MinimalBlockDualInvariantVanishesData D.rawBridge.rawData.rawTowerData

Dual-invariant vanishing obtained from the reassembled actual invariant packet, avoiding minimalBlock_dualInvariantVanishesData.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute157Closers.KernelRoute157RawActualFrattiniFacts.headSimplicityData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute157RawActualFrattiniFacts chief) : MinimalBlockRawHeadSimplicityActualData D.rawBridge.rawData.rawTowerData

Head simplicity obtained from the Route143 nonzero-stable criterion, avoiding minimalBlock_rawHeadSimplicityActualData.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute157Closers.KernelRoute157RawActualFrattiniFacts.rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute157RawActualFrattiniFacts chief) : MinimalBlockRawInvariantCharacterData D.rawBridge.rawData.rawTowerData

Raw invariant character obtained from the reassembled actual invariant packet, avoiding minimalBlock_rawInvariantCharacterData.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute157Closers.KernelRoute157RawActualFrattiniFacts.toRoute152ProvenanceModuleFacts {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute157RawActualFrattiniFacts chief) : Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts chief

Forget Route157 data to Route152's provenance/module bridge shape.

Equations

• D.toRoute152ProvenanceModuleFacts = { least := D.least, frattini := ⋯, rawBridge := D.rawBridge, headAction := ⋯, dualInvariant := ⋯, headSimplicity := ⋯, rawInvariantCharacter := ⋯ }

Lower providers and bridges

theorem Q2Presentation.Induction.Section7KernelRoute157Closers.kernelRoute157RawActualFrattiniFacts_from_lowerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute157RawActualFrattiniFacts chief)

Route157 lower kernel/provenance packet from Route141 Frattini and Route143 raw-actual data.

This theorem is the main kernel lowering surface: its closure should not contain the Route78 selected atoms, the Route141 raw object/action atoms, or the three raw invariant facts listed in the Route156 audit.

theorem Q2Presentation.Induction.Section7KernelRoute157Closers.kernelRoute152ProvenanceModuleFacts_from_section7KernelRoute157Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts chief)

Route152 provenance/module facts supplied by the Route157 lowering.

theorem Q2Presentation.Induction.Section7KernelRoute157Closers.kernelRoute151SelectedPackageData_from_section7KernelRoute157Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Section7KernelRoute151Closers.KernelRoute151SelectedPackageData chief)

Route151 package shape rebuilt through Route152's bridge, with Route157 lower data as the source.

This theorem deliberately uses kernelRoute151SelectedPackageData_of_route152ProvenanceModuleFacts, not the Route151 package axiom and not Route152's existing lower-data theorem.

theorem Q2Presentation.Induction.Section7KernelRoute157Closers.minimalBlock_groupTowerData_from_section7KernelRoute157Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Group-tower provider for Route156 replay with the Route157 kernel bridge.

Route156 replay with only the kernel provider lowered

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

Route156 nonterminal Fourier branch with the kernel packet routed through Route157.

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

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated157KernelRoute152 (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 Route156 with the Route157 kernel lowering.