Route133 Section 7 closers

This sidecar leaves the promoted presentation files untouched. It re-routes the current Route133 nonterminal branch through narrower Section 7 providers:

• kernel/provenance: MinimalBlockInvariantSemanticProofs removes the current direct dual-invariant, raw-head simplicity, and raw invariant-character leaves from the route closure;
• pushout/determinant: MinimalBlockDeterminantPacketProofs2 removes the four semantic determinant leaves by projecting them from the same-family actual simple-head determinant packet.

The candidate and target parts are inherited unchanged from IntegratedCurrentRouteProofs133AllRoute130Lowered.

Kernel/provenance providers

theorem Q2Presentation.Induction.Section7Route133Closers.minimalBlock_dualInvariantVanishesData_from_section7Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockDualInvariantVanishesData D)

Route133 Section 7 replacement for the direct dual-invariant leaf.

The proof is delegated to MinimalBlockInvariantSemanticProofs, which derives the packet from the quotient-head no-trivial-dual interface rather than from minimalBlock_dualInvariantVanishesData.

theorem Q2Presentation.Induction.Section7Route133Closers.minimalBlock_rawInvariantCharacterData_from_section7Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantCharacterData D)

Route133 Section 7 replacement for the raw invariant-character leaf.

The proof is delegated to MinimalBlockInvariantSemanticProofs, which derives the packet from the lower scalar-quotient interface rather than from minimalBlock_rawInvariantCharacterData.

theorem Q2Presentation.Induction.Section7Route133Closers.minimalBlock_groupTowerData_from_section7KernelClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Route133 kernel tower provider through the narrowed invariant-semantic route. This is the provider used by the route theorem below.

Pushout/determinant providers

theorem Q2Presentation.Induction.Section7Route133Closers.minimalBlock_preheadCentralPushoutSemanticDeterminantPackets_from_section7Closers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

The four semantic determinant packets, supplied from the same-family actual simple-head determinant packet.

theorem Q2Presentation.Induction.Section7Route133Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

Route133 determinant-packet provider with the semantic determinant side routed through MinimalBlockDeterminantPacketProofs2.

Route133 audit theorem with Section 7 providers swapped

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

Route133 nonterminal Fourier branch with only the Section 7 providers swapped to this sidecar. Candidate and target realization are exactly the Route133 all-Route130-lowered realization theorem.

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

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

Route133 finite-surjection equality with only the Section 7 providers replaced by this sidecar.