Concrete target marked-quotient proofs

This sidecar closes the current presentation_correct target residuals as far as the existing framed-target API allows, without editing the routed files.

The manuscript tower is

Y -> B = Y/R -> C = Y/K,

with marked-kernel restrictions L_Y -> L_B -> L_C. The current API does not construct quotient framed targets from a raw normal subgroup: it needs data that the quotient targets' marked kernels and decorations are the inherited ones. Accordingly the broad residuals are reduced to the narrower packets already matching that manuscript data:

• middle/lower framed quotient targets;
• actual marked restrictions of the ambient quotient maps;
• the corresponding marked-kernel identifications.

The route-ready theorem at the end mirrors the current actual-closer route, but uses these split packets instead of the three broad residual names.

The three broad residuals, theorem-level from split packets

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientData_from_concreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalQuotientData B D)

Replacement for centralCover_targetCanonicalQuotientData.

The current quotient-target API still needs the two framed quotient children Y/R and Y/K as data. This theorem reassembles the broad packet from those two narrower child packets.

theorem Q2Presentation.Induction.centralCover_targetActualTopMarkedRestrictionData_from_concreteProofs {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetActualTopMarkedRestrictionData B S Q)

Replacement for centralCover_targetActualTopMarkedRestrictionData.

The actual top restriction is exactly the pair consisting of the restricted map L_Y -> L_B, its agreement with Y -> B, and the kernel identification with R.

theorem Q2Presentation.Induction.centralCover_targetActualMiddleMarkedRestrictionData_from_concreteProofs {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetActualMiddleMarkedRestrictionData B S Q)

Replacement for centralCover_targetActualMiddleMarkedRestrictionData.

The actual middle restriction is the restricted map L_B -> L_C, its agreement with B -> C, and the kernel comparison with the ambient middle kernel.

Reassembly lemmas using the replacements above

theorem Q2Presentation.Induction.centralCover_targetQuotientChildConcreteData_from_concreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetQuotientChildConcreteData B (targetSubgroupTowerData_of_concrete B D))

theorem Q2Presentation.Induction.centralCover_targetTopMarkedExactData_from_concreteProofs {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTopMarkedExactData B S Q)

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedExactData_from_concreteProofs {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleMarkedExactData B S Q)

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientTowerData_from_selfGroupTower_concreteProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CentralCoverTargetCanonicalQuotientTowerData (G.toMinimalBlock h F A R))

Canonical target quotient data for a block built from a Section 7 group tower, routed through the split target marked-quotient packets.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerConcreteProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CoverRealization (G.toMinimalBlock h F A R))

Cover realization through the concrete target marked-quotient sidecar.

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

Nonterminal Fourier branch through the concrete target marked-quotient sidecar.

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

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

Equal finite surjection counts through the concrete target marked-quotient sidecar. This is the obvious route target for PresentationCorrect.lean; the file deliberately does not perform that import swap.