Candidate Frattini Route52 proofs

This sidecar is candidate Section 8 only. It does not edit the routed IntegratedCurrentRouteProofs* files.

Route51 exposes the two broad candidate leaves

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

Route52 avoids both names in the routed candidate provider. The lift partition is assembled instead from the current split packets:

• centralCover_candidateMiddleScalarObstructionEvaluatorData, the scalar-pushout evaluator, linear in lambda : X_R;
• centralCover_candidateFrattiniAffineFiberCoordinateData, the coordinate and realization maps for the canonical affine fibres, with the two inverse laws.

These are the smaller manuscript-shaped inputs from def:Xgamma, lem:obstructionseparation, lem:affinelifting, and prop:finalfourier. The arbitrary I, O cardinality packet is deliberately not reconstructed: the manuscript uses the canonical middle exact-image index and the affine fibres attached to the selected obstruction map.

Candidate Route52 provider

theorem Q2Presentation.Induction.centralCover_candidateMiddleRLiftObstructionMapData_from_frattiniRoute52 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateMiddleRLiftObstructionMapData B T)

Route52 middle R-lift obstruction map.

The residual underneath this theorem is the scalar-pushout evaluator from CandidateCurrentSemanticClosers, not the broad obstruction-map packet centralCover_candidateObstructionMapData.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_frattiniRoute52 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F)

Route52 Frattini exact-image partition for the selected obstruction map.

The residual underneath this theorem is the coordinate/realization equivalence for the canonical affine fibres, not the broad arbitrary cardinality packet centralCover_candidateFrattiniExactImageCardinalityData.

theorem Q2Presentation.Induction.centralCover_candidateDirectExactImageResidualData_from_frattiniRoute52 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F)

Coherent Route52 candidate exact-image pair.

This is the actual middle obstruction map together with the matching Frattini partition for the affine fibres attached to that same map.

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

Drop-in Route52 candidate lift-partition provider.

This keeps the public call shape used by Route50/Route51 integration while assembling the partition directly from the canonical middle obstruction map and matching Frattini exact-image partition. The quotient-frame argument is kept for call-site compatibility; the coherent lift-partition packet itself only needs the selected obstruction, canonical fibres, and partition.

Route51 path with only the candidate provider swapped

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCandidateFrattiniRoute52 {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))

Route51 central-cover realization with the candidate side routed through the Route52 split Frattini provider. Target, kernel, local, proper-image, and pushout providers are exactly the Route51 ones.

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

Route52 nonterminal Fourier branch with only the candidate provider replaced by the split Frattini provider.

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

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

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