Candidate Frattini route50 proofs

This sidecar is candidate Section 8 only: it does not edit the routed IntegratedCurrentRouteProofs* files. It keeps the Route49 target, kernel, and pushout providers, but replaces the Route48 candidate provider

• centralCover_candidateMiddleFrattiniResidualProofData

by the two lower manuscript-shaped exact-image packets:

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

The two packets are the Section 8 obstruction-separation map and the final Frattini/Fourier exact-image cardinality statement. The quotient-frame and canonical middle exact-image index are supplied theorem-level by the existing candidate sidecars.

Candidate Route50 provider

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_frattiniRoute50 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Route50 candidate provider with the same public shape as the Route48 candidate provider.

Its axiom closure removes centralCover_candidateMiddleFrattiniResidualProofData and exposes exactly the two lower candidate packets needed by the manuscript's final Frattini exact-image recursion.

Route49 path with only the candidate provider swapped

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

Route49 central-cover realization with the candidate side routed through the Route50 Frattini provider. Target, kernel, local, and proper-image providers are exactly the same as in Route48/49.

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

Route49 nonterminal Fourier branch with only the candidate provider replaced by the Route50 Frattini provider.

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

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

Route50 count theorem. This is not wired into PresentationCorrect; it is an audited sidecar theorem showing the candidate frontier shrink.