Candidate Route138 closers

This sidecar attacks only the Route138 candidate Section 8 leaves. The Route138 integrated proof uses the Route115 scalar/Frattini split:

• centralCover_candidateMiddleScalarPushoutValueData;
• centralCover_candidateMiddleScalarPushoutLinearityData;
• centralCover_candidateFrattiniLiftCoordinateData;
• centralCover_candidateFrattiniRealizationData;
• centralCover_candidateFrattiniCoordinateInverseData.

The arbitrary-linearity and arbitrary-inverse leaf shapes are stronger than the manuscript recursion needs. Section 8 uses a selected middle R-obstruction map on the canonical exact-image index and the matching Frattini exact-image partition. This file routes the candidate contribution through those narrower packets:

• centralCover_candidateMiddleRLiftObstructionMapData_residual;
• centralCover_candidateFrattiniAffineFiberPartition_residual.

It leaves all public route files untouched.

Selected scalar projections from the lower middle obstruction

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route138ScalarPushoutValueData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateMiddleScalarPushoutValueData B T

Route138 scalar-pushout values obtained by evaluating the selected R-valued obstruction against invariant scalar pushouts.

Equations

• D.route138ScalarPushoutValueData = { scalarPushoutValue := fun (lam : ↥B.XR) (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => (D.obstruction x) lam }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route138ScalarPushoutLinearityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateMiddleScalarPushoutLinearityData D.route138ScalarPushoutValueData

Route138 linearity for the selected scalar-pushout value family.

Equations

• D.route138ScalarPushoutLinearityData = { map_add := ⋯, map_smul := ⋯ }

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

The Route138 scalar value leaf follows from the lower selected R-obstruction map.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutSelectedLinearityData_from_candidateRoute138Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((D : CentralCoverCandidateMiddleScalarPushoutValueData B T) × CentralCoverCandidateMiddleScalarPushoutLinearityData D)

Selected Route138 scalar value and linearity data.

This is the manuscript-shaped replacement for the overbroad arbitrary-linearity leaf: linearity is supplied for the scalar family induced by the selected middle R-obstruction map.

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

Current scalar-obstruction evaluator assembled from the selected lower middle R-obstruction map.

Selected Frattini coordinates from the lower exact-image partition

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route138LiftCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniLiftCoordinateData B T D

Route138 lift-coordinate map carried by the selected exact-image partition.

Equations

• P.route138LiftCoordinateData = { liftCoordinate := ⇑P.partition.bij }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route138RealizationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniRealizationData B T D

Route138 realization map carried by the inverse exact-image partition.

Equations

• P.route138RealizationData = { realizeCoordinate := P.partition.bij.invFun }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route138CoordinateInverseData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniCoordinateInverseData P.route138LiftCoordinateData P.route138RealizationData

Route138 inverse laws for the selected coordinate and realization maps.

Equations

• P.route138CoordinateInverseData = { realize_liftCoordinate := ⋯, liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route138AffineFiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D

The current Frattini coordinate packet induced by the selected exact-image partition.

Equations

• P.route138AffineFiberCoordinateData = P.route138LiftCoordinateData.coordinateData P.route138RealizationData P.route138CoordinateInverseData

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

The Route138 Frattini lift-coordinate leaf follows from the lower selected exact-image partition.

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

The Route138 Frattini realization leaf follows from the inverse of the lower selected exact-image partition.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniSelectedCoordinateInverseData_from_candidateRoute138Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) × (R : CentralCoverCandidateFrattiniRealizationData B T D) × CentralCoverCandidateFrattiniCoordinateInverseData L R)

Selected Route138 coordinate, realization, and inverse laws.

This is the manuscript-shaped replacement for the overbroad arbitrary-inverse leaf: the inverse laws are supplied for the coordinate and realization maps coming from the same exact-image partition.

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

The current Frattini affine-fibre coordinate packet induced by the lower selected exact-image partition.

Route-ready candidate provider

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

Route138 direct exact-image residual data, using the selected middle R-obstruction and matching Frattini partition.

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

Drop-in Route138 candidate lift-partition provider.

The downstream call shape matches the Route135/138 call site with a supplied quotient-frame map, but the closure avoids all five Route138 candidate leaves.

Integrated Route139 candidate-lowered route

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

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

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

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