Semantic simple-head and scalar closers for Section 7

This sidecar owns the simple-head/scalar part of the Section 7 route. It keeps the routed files untouched and replaces the four exposed packets

• minimalBlock_rawInvariantNonzeroFunctionalsKillTData;
• minimalBlock_rawHeadOrbitSpansData;
• minimalBlock_rawHeadActionNontrivialData;
• minimalBlock_rawLowerNonzeroInvariantCharacterData;

by smaller manuscript-shaped residuals:

• invariant hyperplanes cannot miss T;
• the quotient head has no nonzero proper stable submodule;
• the quotient-head action is not pointwise trivial;
• the lower scalar layer has a nonzero invariant character.

The conversion lemmas below do the remaining linear algebra in Lean.

Invariant functionals kill the lower layer

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

Minimality form of the manuscript argument: no nonzero invariant functional on M can detect an element of T.

• 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

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

Actual-packet closer: invariant hyperplanes contain the lower layer.

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

Nonzero invariant functionals on M vanish on the lower layer T.

• invariant_nonzero_functionals_kill_T (phi : Module.Dual (ZMod 2) D.M) : phi ≠ 0 → (∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) → ∀ t ∈ D.T, phi t = 0

def Q2Presentation.Induction.MinimalBlockRawInvariantNonzeroFunctionalsKillTData.ofHyperplanesContainT {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (H : MinimalBlockRawInvariantHyperplanesContainTData D) : MinimalBlockRawInvariantNonzeroFunctionalsKillTData D

The routed nonzero-functional packet follows from the hyperplane/minimality form.

Equations

• ⋯ = ⋯

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

Routed packet, now derived from the semantic hyperplane residual.

def Q2Presentation.Induction.MinimalBlockRawInvariantFunctionalsKillTData.ofNonzeroKillT {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (K : MinimalBlockRawInvariantNonzeroFunctionalsKillTData D) : MinimalBlockRawInvariantFunctionalsKillTData D

The existing all-functional packet follows from its nonzero-kernel form; the zero functional case is discharged in Lean.

Equations

• ⋯ = ⋯

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

The quotient head is irreducible

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

Irreducibility form of the first non-scalar simple head.

• eq_top_of_nonzero_stable (U : Submodule (ZMod 2) (D.M ⧸ D.T)) : minimalBlock_rawHeadStable D U → (∃ x ∈ U, x ≠ 0) → U = ⊤

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

Actual-packet closer: the quotient head is a simple nonzero C-module.

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

Every nonzero vector in the raw quotient head generates the whole head under the C-action.

• orbit_span_eq_top (x : D.M ⧸ D.T) : x ≠ 0 → Submodule.span (ZMod 2) (Set.range fun (c : D.C) => (minimalBlock_rawHeadAction D c) x) = ⊤

def Q2Presentation.Induction.MinimalBlockRawHeadOrbitSpansData.ofIrreducible {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockRawHeadIrreducibleData D) : MinimalBlockRawHeadOrbitSpansData D

The routed orbit-span packet follows from irreducibility of the quotient head.

Equations

• ⋯ = ⋯

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

Routed packet, now derived from the semantic irreducibility residual.

def Q2Presentation.Induction.MinimalBlockRawHeadNonzeroStableEqTopData.ofOrbitSpans {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockRawHeadOrbitSpansData D) : MinimalBlockRawHeadNonzeroStableEqTopData D

The existing nonzero-stable-submodule criterion follows from orbit spanning.

Equations

• ⋯ = ⋯

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

Dual invariants vanish on the quotient head

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

Semantic form of nontriviality: the quotient-head action is not pointwise trivial.

• not_pointwise_trivial : ¬∀ (c : D.C) (x : D.M ⧸ D.T), (minimalBlock_rawHeadAction D c) x = x

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

Actual-packet closer: the first non-scalar head is not a trivial C-module.

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

The quotient-head action is not the trivial action.

• head_action_nontrivial : ∃ (c : D.C) (x : D.M ⧸ D.T), (minimalBlock_rawHeadAction D c) x ≠ x

def Q2Presentation.Induction.MinimalBlockRawHeadActionNontrivialData.ofNotPointwiseTrivial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockRawHeadActionNotPointwiseTrivialData D) : MinimalBlockRawHeadActionNontrivialData D

The routed nontrivial-action packet follows from the not-pointwise-trivial semantic form.

Equations

• ⋯ = ⋯

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

Routed packet, now derived from the not-pointwise-trivial residual.

def Q2Presentation.Induction.MinimalBlockRawHeadDualInvariantZeroData.ofNonzeroStableActionNontrivial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockRawHeadNonzeroStableEqTopData D) (A : MinimalBlockRawHeadActionNontrivialData D) : MinimalBlockRawHeadDualInvariantZeroData D

Orbit simplicity plus a nontrivial head action proves that the dual head has no invariant functional.

Equations

• ⋯ = ⋯

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

Lower scalar quotient from a nonzero invariant character

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

Existential form of the lower scalar-layer character.

• exists_nonzero_invariant : ∃ (character : Module.Dual (ZMod 2) D.R), character ≠ 0 ∧ ∀ (c : D.C), character ∘ₗ ↑(D.actR c) = character

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

Actual-packet closer: the lower scalar layer has a nonzero invariant character.

structure Q2Presentation.Induction.MinimalBlockRawLowerNonzeroInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Type

A nonzero invariant character on the lower Frattini layer R.

• character : Module.Dual (ZMod 2) D.R
• character_ne_zero : self.character ≠ 0
• character_invariant (c : D.C) : self.character ∘ₗ ↑(D.actR c) = self.character

def Q2Presentation.Induction.MinimalBlockRawLowerNonzeroInvariantCharacterData.ofExists {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (X : MinimalBlockRawLowerInvariantCharacterExistsData D) : MinimalBlockRawLowerNonzeroInvariantCharacterData D

Choose a concrete lower character from the existential semantic packet.

Equations

• Q2Presentation.Induction.MinimalBlockRawLowerNonzeroInvariantCharacterData.ofExists X = { character := Classical.choose ⋯, character_ne_zero := ⋯, character_invariant := ⋯ }

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

Routed packet, now derived from the existential lower-character residual.

def Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData.ofNonzeroInvariantCharacter {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (X : MinimalBlockRawLowerNonzeroInvariantCharacterData D) : MinimalBlockRawLowerScalarQuotientData D

A nonzero invariant lower character gives the current scalar quotient packet.

Equations

• Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData.ofNonzeroInvariantCharacter X = { quotient := X.character, quotient_surjective := ⋯, quotient_invariant := ⋯ }

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

Same-tower reassembly through the smaller packets

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

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

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

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

Concrete-final provenance pieces through the semantic simple-head/scalar split in this sidecar.

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

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

Final-count route with only this sidecar's simple-head/scalar packets

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

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

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