Concrete final provenance closers for the Section 7 minimal block

This sidecar pushes one step beyond MinimalBlockProvenanceFinalClosers. The earlier final closer assembled minimalBlock_provenanceSemanticData from Curie's four packets:

• concrete subgroup/module provenance;
• quotient-head no-trivial-dual data;
• quotient-head simplicity;
• lower scalar quotient data.

Here the same selected concrete K/R tower is used, but the quotient-head no-trivial and lower scalar quotient packets are rebuilt from the still smaller raw ingredients on that tower:

• direct (M^vee)^C = 0 dual-invariant vanishing;
• raw nonzero invariant determinant character in (R^vee)^C.

Raw invariant characters give actual lower characters

def Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData.ofRawInvariantCharacter {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (X : MinimalBlockRawInvariantCharacterData D) : MinimalBlockRawLowerInvariantCharacterActualData D

A nonzero raw invariant character over F_2 gives the actual lower invariant-character packet needed by MinimalBlockProvenanceSemanticData.

Equations

• Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData.ofRawInvariantCharacter X = { character := Classical.choose ⋯, character_hits_one := ⋯, character_invariant := ⋯ }

Concrete final selected-tower packet

structure Q2Presentation.Induction.MinimalBlockProvenanceConcreteFinalPieces {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Final provenance pieces on the single raw tower forced by the concrete subgroup/module provenance.

Compared with MinimalBlockProvenanceFinalPieces, this replaces the two derived packets MinimalBlockRawHeadQuotientNoTrivialData and MinimalBlockRawLowerScalarQuotientData by their lower raw sources: direct dual-invariant vanishing and a raw invariant determinant character.

• concrete : MinimalBlockKernelModuleConcreteProvenanceData chief
• dualInvariant : MinimalBlockDualInvariantVanishesData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData
• headSimplicity : MinimalBlockRawHeadSimplicityActualData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData
• rawInvariantCharacter : MinimalBlockRawInvariantCharacterData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData

def Q2Presentation.Induction.MinimalBlockProvenanceConcreteFinalPieces.lower {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceConcreteFinalPieces chief) : MinimalBlockLowerGroupModuleData chief

The selected lower tower extracted from the concrete provenance.

Equations

• P.lower = Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance P.concrete

def Q2Presentation.Induction.MinimalBlockProvenanceConcreteFinalPieces.headNoTrivial {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceConcreteFinalPieces chief) : MinimalBlockRawHeadQuotientNoTrivialData P.lower.rawTowerData

The quotient-head no-trivial-dual packet rebuilt from direct dual-invariant vanishing on the selected tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceConcreteFinalPieces.headActual {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceConcreteFinalPieces chief) : MinimalBlockRawHeadSimpleNoTrivialActualData P.lower.rawTowerData

The actual simple/no-trivial head packet on the selected lower tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceConcreteFinalPieces.lowerCharacter {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceConcreteFinalPieces chief) : MinimalBlockRawLowerInvariantCharacterActualData P.lower.rawTowerData

The actual lower invariant-character packet rebuilt directly from the raw invariant determinant character.

Equations

• P.lowerCharacter = Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData.ofRawInvariantCharacter ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceConcreteFinalPieces.toProvenanceSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceConcreteFinalPieces chief) : MinimalBlockProvenanceSemanticData chief

Convert the concrete-final pieces into the broad provenance-semantic packet used by the current final route.

Equations

• P.toProvenanceSemanticData = { concrete := P.concrete, lower := P.lower, lower_eq_concrete := ⋯, headActual := ⋯, lowerCharacter := P.lowerCharacter }

Closers

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

The concrete-final packet follows from concrete provenance, direct dual-invariant vanishing, quotient-head simplicity, and raw invariant character, all on the raw tower forced by the concrete provenance.

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

Route-ready replacement for minimalBlock_provenanceSemanticData.

Its axiom closure no longer contains Curie's minimalBlock_rawHeadQuotientNoTrivialData or minimalBlock_rawLowerScalarQuotientData; those two packets are rebuilt on the selected concrete tower from direct dual-invariant vanishing and raw invariant character data.

theorem Q2Presentation.Induction.minimalBlock_rawHeadQuotientNoTrivialData_from_concreteFinalProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (lower : MinimalBlockLowerGroupModuleData chief), Nonempty (MinimalBlockRawHeadQuotientNoTrivialData lower.rawTowerData)

The selected quotient-head no-trivial packet obtained without using the raw no-trivial packet axiom.

theorem Q2Presentation.Induction.minimalBlock_rawLowerScalarQuotientData_from_concreteFinalProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (lower : MinimalBlockLowerGroupModuleData chief), Nonempty (MinimalBlockRawLowerScalarQuotientData lower.rawTowerData)

The selected lower scalar quotient packet obtained without using the raw lower scalar quotient packet axiom.

theorem Q2Presentation.Induction.minimalBlock_rawHeadSimplicityActualData_from_concreteFinalProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (lower : MinimalBlockLowerGroupModuleData chief), Nonempty (MinimalBlockRawHeadSimplicityActualData lower.rawTowerData)

The selected quotient-head simplicity packet for the concrete-final tower.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteProvenanceData_from_concreteFinalProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

The selected concrete provenance packet for the concrete-final tower.

theorem Q2Presentation.Induction.minimalBlock_groupInvariantRouteData_from_concreteFinalProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Group/invariant route data through the concrete-final provenance theorem.

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

The group tower consumed by determinant and central-cover routes, through the concrete-final provenance theorem.