Candidate Frattini Route54 proofs

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

Route53 exposes seven independent candidate residuals:

• pointwise scalar-pushout values and additivity;
• base/fibre Frattini coordinates, fibre realization, and the two inverse laws.

Those are stronger than the route needs, because the manuscript's final Frattini step uses one selected middle R-obstruction and the matching exact-image partition of its unobstructed affine fibres. Route54 therefore packages precisely that coherent exact-image datum and proves the same drop-in lift-partition provider shape consumed by Route53.

Route54 coherent exact-image packet

structure Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Route54 candidate exact-image datum.

This is the route-needed Section 8 object: the middle R-valued obstruction on the canonical middle exact-image source, together with the Frattini exact-image equivalence for the affine fibres attached to that same obstruction.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

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

Route54 residual closed from the Route53 manuscript-shaped split.

Route53 already supplies the selected middle R-obstruction together with the matching Frattini exact-image partition. The Route54 packet asks for the same coherent data with the Frattini component in equivalence form, and the partition stores exactly such a bijection.

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.scalarPushoutValueAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) (lam : ↥B.XR) : CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam

Scalar-pushout value at lambda, obtained by evaluating the selected middle obstruction.

Equations

• D.scalarPushoutValueAtData lam = { valueAt := fun (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => (D.middleObstruction.obstruction x) lam }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.scalarPushoutFamilyData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateMiddleScalarPushoutFamilyData B T

The selected scalar-pushout family induced by the middle obstruction.

Equations

• D.scalarPushoutFamilyData = { valueAt := fun (lam : ↥B.XR) => D.scalarPushoutValueAtData lam }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.scalarPushoutAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateMiddleScalarPushoutAdditivityData D.scalarPushoutFamilyData

Additivity in lambda, inherited from the linear-map structure of B.obstructionSpace.

Equations

• D.scalarPushoutAdditivityData = { map_add := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.scalarPushoutHomogeneityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateMiddleScalarPushoutHomogeneityData D.scalarPushoutFamilyData

Homogeneity in lambda, inherited from the linear-map structure of B.obstructionSpace.

Equations

• D.scalarPushoutHomogeneityData = { map_smul := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.scalarObstructionEvaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

Route52/Route53 scalar evaluator shape recovered from the coherent Route54 datum.

Equations

• D.scalarObstructionEvaluatorData = D.scalarPushoutFamilyData.evaluatorData D.scalarPushoutAdditivityData D.scalarPushoutHomogeneityData

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.frattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.middleObstruction.obstructionIndexToBaseMapData.O D.middleObstruction.affineFiberTorsorData.Z D.middleObstruction.affineFiberTorsorData.F

Frattini exact-image partition carried by the Route54 equivalence.

Equations

• D.frattiniExactImage = D.frattiniEquiv.frattiniExactImage

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.baseCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateFrattiniBaseCoordinateData B T D.middleObstruction

Base coordinate induced by the exact-image equivalence.

Equations

• D.baseCoordinateData = { baseCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (D.frattiniEquiv.equiv f).fst }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.fiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateFrattiniFiberCoordinateData D.baseCoordinateData

Fibre coordinate induced by the exact-image equivalence.

Equations

• D.fiberCoordinateData = { fiberCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (D.frattiniEquiv.equiv f).snd }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.fiberRealizationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateFrattiniFiberRealizationData B T D.middleObstruction

Curried realization induced by the inverse exact-image equivalence.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.realizeLiftCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateFrattiniRealizeLiftCoordinateData D.baseCoordinateData D.fiberCoordinateData D.fiberRealizationData

Realization after Route54 coordinates is the original top exact-image map.

Equations

• D.realizeLiftCoordinateData = { realize_liftCoordinate := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.liftCoordinateRealizeData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateFrattiniLiftCoordinateRealizeData D.baseCoordinateData D.fiberCoordinateData D.fiberRealizationData

Route54 coordinates after realization recover the original affine-fibre point.

Equations

• D.liftCoordinateRealizeData = { liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.affineFiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D.middleObstruction

The current coordinate/realization packet recovered from the Route54 exact-image equivalence.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.CentralCoverCandidateRoute54ExactImageData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute54ExactImageData B T) : CentralCoverCandidateLiftPartitionData B

Candidate lift partition recovered from the coherent exact-image datum.

Equations

• One or more equations did not get rendered due to their size.

Projections from the Route54 packet

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

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

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

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

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

Drop-in Route54 candidate lift-partition provider.

This has the same public call shape as the Route53 candidate provider, but its candidate closure is the single coherent Route54 exact-image packet.

Route53 path with only the candidate provider swapped to Route54

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

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

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

Route54 nonterminal Fourier branch with only the candidate provider replaced by the coherent exact-image route.

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

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

Route54 count theorem. This is an audited sidecar theorem showing the Route53 candidate seven-leaf frontier has been replaced by one coherent exact-image packet; it is not wired into PresentationCorrect.