Actual simple-head/scalar closers for Section 7

This sidecar is the compatibility layer between the actual same-tower Section 7 packet and the current four simple-head/scalar residual names used by MinimalBlockSimpleHeadSemanticClosers.

It uses the existing actual packet minimalBlock_invariantActualProofs2Data, whose fields are attached to one raw tower:

• invariant kernels contain T;
• the quotient head is simple;
• the quotient-head action is nontrivial;
• the lower Frattini layer has an invariant character hitting 1.

The semantic closer converts those direct fields into its four public residual interfaces without routing through the older orbit-span/nonzero-character packet names.

Same-tower actual packet

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

The actual simple-head/scalar packet needed by the current semantic closer.

This is intentionally just a projection of the existing same-raw-tower actual packet, under a name local to the simple-head/scalar sidecar.

• headActual : MinimalBlockRawHeadSimpleNoTrivialActualData D
• lowerCharacter : MinimalBlockRawLowerInvariantCharacterActualData D

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

Existing-API construction of the actual simple-head/scalar packet.

theorem Q2Presentation.Induction.MinimalBlockSimpleHeadActualClosersData.no_invariant_hyperplane_misses_T {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockSimpleHeadActualClosersData D) : ¬∃ (phi : Module.Dual (ZMod 2) D.M), phi ≠ 0 ∧ (∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) ∧ ∃ t ∈ D.T, phi t ≠ 0

Invariant hyperplanes cannot miss the lower layer T.

theorem Q2Presentation.Induction.MinimalBlockSimpleHeadActualClosersData.eq_top_of_nonzero_stable {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockSimpleHeadActualClosersData D) (U : Submodule (ZMod 2) (D.M ⧸ D.T)) : minimalBlock_rawHeadStable D U → (∃ x ∈ U, x ≠ 0) → U = ⊤

The head-simple field gives the nonzero-stable-submodule irreducibility criterion used by the current route.

theorem Q2Presentation.Induction.MinimalBlockSimpleHeadActualClosersData.not_pointwise_trivial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockSimpleHeadActualClosersData D) : ¬∀ (c : D.C) (x : D.M ⧸ D.T), (minimalBlock_rawHeadAction D c) x = x

The actual nontrivial-action witness is equivalent to the route's not-pointwise-trivial formulation.

theorem Q2Presentation.Induction.MinimalBlockSimpleHeadActualClosersData.lower_character_ne_zero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockSimpleHeadActualClosersData D) : A.lowerCharacter.character ≠ 0

A character hitting 1 is nonzero.

theorem Q2Presentation.Induction.MinimalBlockSimpleHeadActualClosersData.exists_nonzero_invariant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockSimpleHeadActualClosersData D) : ∃ (character : Module.Dual (ZMod 2) D.R), character ≠ 0 ∧ ∀ (c : D.C), character ∘ₗ ↑(D.actR c) = character

The lower scalar layer supplies a nonzero invariant character.