Provenance-semantic Section 7 minimal-block route

This sidecar targets the four Section 7 residuals that still appear in the current final closure:

• minimalBlock_kernelModuleConcreteProvenanceData;
• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawHeadSimplicityActualData;
• minimalBlock_rawLowerScalarQuotientData.

The replacement below is one same-tower semantic packet. It fixes the concrete subgroup/module provenance for R = Phi(K) <= K, a coherent lower tower derived from that provenance, and the actual head/lower scalar facts on that selected raw tower. The final route consumes only the resulting MinimalBlockGroupTowerData, so the four older residual names can be kept out of presentation_correct.

Same-tower provenance and invariant packet

def Q2Presentation.Induction.MinimalBlockRawHeadSimplicityActualData.ofSimpleNoTrivialActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (H : MinimalBlockRawHeadSimpleNoTrivialActualData D) : MinimalBlockRawHeadSimplicityActualData D

Head simplicity is a projection of the actual simple/no-trivial head packet.

The actual packet also carries the invariant-kernel containment and nontrivial head action used to prove no trivial dual quotient.

Equations

• ⋯ = ⋯

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

Coherent Section 7 provenance for the final route.

The concrete field is the subgroup-level provenance for K, R = Phi(K), M = K/R, T, C, and the quotient bridge. The lower field is the routed lower tower, with an equality recording that it is the tower obtained from the same concrete provenance. The two invariant fields are then attached to lower.rawTowerData, so the head and lower scalar facts cannot be selected on a different raw tower.

• concrete : MinimalBlockKernelModuleConcreteProvenanceData chief
• lower : MinimalBlockLowerGroupModuleData chief
• lower_eq_concrete : self.lower = (MinimalBlockKernelModuleConcreteBundle.ofProvenance self.concrete).actualProofs.lowerGroupModuleData
• headActual : MinimalBlockRawHeadSimpleNoTrivialActualData self.lower.rawTowerData
• lowerCharacter : MinimalBlockRawLowerInvariantCharacterActualData self.lower.rawTowerData

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

The selected quotient-head no-trivial-dual packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceSemanticData.headSimplicityData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceSemanticData chief) : MinimalBlockRawHeadSimplicityActualData P.lower.rawTowerData

The selected quotient-head simplicity packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceSemanticData.lowerScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceSemanticData chief) : MinimalBlockRawLowerScalarQuotientData P.lower.rawTowerData

The selected lower scalar quotient packet.

Equations

• P.lowerScalarQuotientData = Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData.ofInvariantCharacterActual P.lowerCharacter

def Q2Presentation.Induction.MinimalBlockProvenanceSemanticData.dualInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceSemanticData chief) : MinimalBlockDualInvariantVanishesData P.lower.rawTowerData

Dual-invariant vanishing on the selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceSemanticData.rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceSemanticData chief) : MinimalBlockRawInvariantCharacterData P.lower.rawTowerData

A raw nonzero invariant character on the selected Frattini layer.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceSemanticData.groupInvariantRouteData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceSemanticData chief) : MinimalBlockGroupInvariantRouteData chief

The smaller group/invariant route packet selected by the provenance-semantic data.

Equations

• P.groupInvariantRouteData = { lower := P.lower, dualInvariant := ⋯, rawInvariantCharacter := ⋯ }

def Q2Presentation.Induction.MinimalBlockProvenanceSemanticData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceSemanticData chief) : MinimalBlockGroupTowerData p chief

The group tower consumed by the current determinant and central-cover routes.

Equations

• P.groupTowerData = P.groupInvariantRouteData.groupTowerData

axiom Q2Presentation.Induction.minimalBlock_provenanceSemanticData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Residual same-tower Section 7 provenance packet.

This replaces the four older residual calls in the final route by one coherent object: concrete subgroup provenance plus actual head/lower invariant facts on the raw tower selected from that provenance.

Route-ready projections for the four old residual names

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

Route-ready replacement for minimalBlock_kernelModuleConcreteProvenanceData.

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

Route-ready selected-tower replacement for minimalBlock_rawHeadQuotientNoTrivialData.

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

Route-ready selected-tower replacement for minimalBlock_rawHeadSimplicityActualData.

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

Route-ready selected-tower replacement for minimalBlock_rawLowerScalarQuotientData.

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

The group/invariant route packet with the four old residuals replaced by the same-tower provenance-semantic packet.

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

The group tower used by the final Section 7 route, through the provenance-semantic packet.

Final route with only the Section 7 group tower swapped

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

Nonterminal Fourier branch for the current target/candidate/determinant route, with the Section 7 group tower supplied by the provenance-semantic packet.

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

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

Current finite-surjection theorem with the four named Section 7 residuals replaced by minimalBlock_provenanceSemanticData.