Route12 head/invariant semantic refinements for Section 7

This sidecar keeps the integrated route files untouched. It reuses the theorem-level simple-head/scalar closers to replace the four route12 head/invariant semantic packets

• minimalBlock_rawHeadDualInvariantZeroData;
• minimalBlock_rawHeadNonzeroStableEqTopData;
• minimalBlock_rawInvariantCharacterData;
• minimalBlock_rawInvariantFunctionalsKillTData.

The replacement is the manuscript split from Section 7: invariant hyperplanes contain T, the quotient head is irreducible and nontrivial, and the lower Frattini layer carries a nonzero invariant character. The exported group-tower provider below is compatible with IntegratedCurrentRouteProofs12.

Same-raw-tower semantic packet

structure Q2Presentation.Induction.MinimalBlockHeadInvariantSemanticRoute12Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

One same-raw-tower semantic packet for the Section 7 simple-head/invariant layer.

The fields are the manuscript-shaped inputs behind lem:simplehead and the lower scalar layer:

• invariant hyperplanes in M contain T;
• every nonzero stable submodule of the quotient head is the whole head;
• the quotient-head action is not pointwise trivial;
• R has a nonzero C-invariant character.

This is intentionally narrower than the old route-facing packet names and is attached to one selected raw tower.

• no_invariant_hyperplane_misses_T : ¬∃ (phi : Module.Dual (ZMod 2) D.M), phi ≠ 0 ∧ (∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) ∧ ∃ t ∈ D.T, phi t ≠ 0
• eq_top_of_nonzero_stable (U : Submodule (ZMod 2) (D.M ⧸ D.T)) : minimalBlock_rawHeadStable D U → (∃ x ∈ U, x ≠ 0) → U = ⊤
• not_pointwise_trivial : ¬∀ (c : D.C) (x : D.M ⧸ D.T), (minimalBlock_rawHeadAction D c) x = x
• exists_nonzero_invariant : ∃ (character : Module.Dual (ZMod 2) D.R), character ≠ 0 ∧ ∀ (c : D.C), character ∘ₗ ↑(D.actR c) = character

axiom Q2Presentation.Induction.minimalBlock_headInvariantSemanticRoute12Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockHeadInvariantSemanticRoute12Data D)

Residual semantic packet replacing the four route12 head/invariant residual names on one selected raw tower.

Direct route12 packet replacements

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

Route12 replacement for invariant functionals killing the lower scalar layer T, proved through the simple-head/scalar semantic split.

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

Route12 replacement for vanishing of dual invariants on the quotient head.

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

Route12 replacement for quotient-head irreducibility in the nonzero-stable-submodule form.

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

Route12 replacement for the raw invariant Frattini character packet.

Same-tower reassembly for route12

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

Dual-invariant vanishing on the same raw tower, assembled from the route12 semantic head packets above.

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

Head simplicity in the route10/route12 actual packet form, assembled from the route12 semantic irreducibility replacement.

theorem Q2Presentation.Induction.minimalBlock_provenanceConcreteFinalPieces_from_headInvariantSemanticRoute12Proofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance pieces with the four route12 head/invariant packet names replaced by the semantic simple-head/scalar closers.

theorem Q2Presentation.Induction.minimalBlock_provenanceSemanticData_from_headInvariantSemanticRoute12Proofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Provenance semantic data with the route12 head/invariant semantic split.

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

Route-ready group tower for IntegratedCurrentRouteProofs12, with the four head/invariant packet names removed from this provider and replaced by the semantic simple-head/scalar split.

Route12 compatibility theorem

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

Route12 nonterminal branch with only the group-tower provider swapped to the head/invariant semantic route12 sidecar.

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

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

Route12 finite-surjection equality with the head/invariant group-tower provider routed through this semantic sidecar.

Removed/refined residual names for this route12 sidecar:

• minimalBlock_rawHeadDualInvariantZeroData;
• minimalBlock_rawHeadNonzeroStableEqTopData;
• minimalBlock_rawInvariantCharacterData;
• minimalBlock_rawInvariantFunctionalsKillTData.