Route10 head/invariant refinements for Section 7

This route-neutral sidecar targets the three route10 P4 residuals

• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawHeadSimplicityActualData;
• minimalBlock_rawLowerScalarQuotientData.

The manuscript input is Section 7, especially lem:simplehead: invariant functionals kill the lower layer T, the quotient head M/T is the first non-scalar simple head, and nonzero invariant characters on the Frattini layer give the scalar quotients needed downstream.

The proofs below do not close the finite group theory itself. They replace the three broad route10 residual names by four smaller semantic packets already exposed by the nearby concrete sidecars:

• invariant functionals on M kill T;
• the quotient head has no invariant dual;
• every nonzero stable head submodule is all of the head;
• the Frattini layer has a raw nonzero invariant character.

Direct replacements for the three P4 residuals

theorem Q2Presentation.Induction.minimalBlock_rawHeadQuotientNoTrivialData_from_route10HeadInvariantProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadQuotientNoTrivialData D)

Route10 replacement for the raw no-trivial-head packet, assembled from the two manuscript-shaped dual packets.

theorem Q2Presentation.Induction.minimalBlock_rawHeadSimplicityActualData_from_route10HeadInvariantProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadSimplicityActualData D)

Route10 replacement for quotient-head simplicity, reduced to the standard nonzero-stable-submodule criterion.

theorem Q2Presentation.Induction.minimalBlock_rawLowerScalarQuotientData_from_route10HeadInvariantProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerScalarQuotientData D)

Route10 replacement for the lower scalar quotient, reduced to a raw nonzero invariant character on R; surjectivity is automatic over ZMod 2.

Same-tower assembly for the route10 group tower

theorem Q2Presentation.Induction.minimalBlock_rawLowerInvariantCharacterActualData_from_route10HeadInvariantProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterActualData D)

Lower actual invariant-character data from the same raw invariant character used to build the lower scalar quotient.

theorem Q2Presentation.Induction.minimalBlock_rawHeadSimpleNoTrivialActualData_from_route10HeadInvariantProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockRawHeadSimpleNoTrivialActualData D.rawTowerData)

Same-tower actual simple-head packet for a selected lower group/module tower.

The nontriviality field is taken from D, so the head packet remains attached to the same raw tower selected by the route10 kernel/Frattini construction.

theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_from_route10HeadInvariantProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D.rawTowerData)

Route10 replacement for minimalBlock_invariantActualProofs2Data, with the three broad P4 residuals replaced by the smaller semantic packets above.

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

Route10 group tower with the P3 kernel/Frattini route unchanged and the P4 head/invariant layer supplied by this sidecar.

Route10 finite-surjection theorem with only the P4 group tower swapped

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

Route10 nonterminal branch with the head/invariant sidecar replacing the route10 P4 residual calls.

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

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

Route-ready finite-surjection equality for route10 with the P4 residual names removed from this theorem's axiom closure.