Candidate Frattini Route53 proofs

This sidecar is candidate Section 8 only at the provider surface, and it does not edit any integrated route files.

Route52 exposed the two current candidate leaves

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

Route53 proves those two packet shapes from the lower scalar-pushout and Frattini coordinate constructors already isolated in the candidate sidecars:

• pointwise scalar-pushout values and additivity in lambda : X_R, with ZMod 2 homogeneity proved theorem-level;
• base coordinate, affine fibre coordinate, curried realization, and the two inverse laws for the final Frattini affine fibre.

The exported provider has the same call shape as centralCover_candidateLiftPartitionData_from_frattiniRoute52, but its axiom closure no longer contains the two Route52 candidate leaves.

Route53 wrappers for the two Route52 candidate leaves

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

Route53 middle scalar obstruction evaluator.

This has the same target type as the Route52 candidate scalar leaf, but its closure is the lower pointwise scalar-pushout value family plus additivity. Homogeneity over ZMod 2 is supplied theorem-level by Route36.

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

Route53 middle R-lift obstruction map assembled from the lower scalar pushout route.

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

Route53 Frattini affine-fibre coordinate data.

This has the same target type as the Route52 candidate Frattini leaf, but its closure is the lower base coordinate, fibre coordinate, realization map, and the two inverse-law packets.

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

Route53 Frattini exact-image partition for the selected middle obstruction map.

theorem Q2Presentation.Induction.centralCover_candidateDirectExactImageResidualData_from_frattiniRoute53 {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 Route53 candidate exact-image pair.

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

Drop-in Route53 candidate lift-partition provider.

This is compatible with the Route52 provider surface: B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B).

Route52 path with only the candidate provider swapped to Route53

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

Route53 central-cover realization: Route52 target, kernel, and pushout providers, with the candidate lift partition routed through Route53.

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

Route53 nonterminal Fourier branch with only the candidate provider replaced by the lower scalar/Frattini coordinate route.

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

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

Route53 count theorem. This is an audited sidecar theorem showing the candidate Route52 leaves have been replaced by lower scalar/Frattini coordinate packets; it is not wired into PresentationCorrect.