Candidate Route100 coherent closers

This sidecar is candidate Section 8 only. It does not edit IntegratedCurrentRouteProofs100.

Route100 currently calls

centralCover_candidateLiftPartitionData_from_route98

whose candidate closure exposes the two coherent residuals

• centralCover_candidateMiddleScalarPushoutCoherentData;
• centralCover_candidateFrattiniCoordinateCoherentData.

The theorems below lower those two residuals to the actual manuscript-shaped middle obstruction and Frattini exact-image packets from CandidateMiddleFrattiniActualProofs, then provide a Route100-shaped branch and count theorem with only the candidate provider swapped.

Route100 candidate packet-level closers

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

Route100 scalar coherent packet from the actual middle R-obstruction.

The selected scalar-pushout evaluator is obtained by evaluating the actual R-valued obstruction against lambda : X_R; linearity is inherited from the linear-map structure of that obstruction.

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

Route100 Frattini coordinate coherent packet from the actual Frattini exact-image equivalence for the supplied middle obstruction.

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

Direct exact-image residual data from the actual middle obstruction and the matching actual Frattini exact-image equivalence.

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

Route100 drop-in candidate lift-partition provider.

This has the same call shape as centralCover_candidateLiftPartitionData_from_route98, but its candidate closure is the two actual Section 8 packets instead of the two Route100 coherent residual names.

Route100 branch with only the candidate provider swapped

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

Route100 realization proof with the candidate lift partition routed through centralCover_candidateLiftPartitionData_from_route100CoherentClosers.

All target, kernel, and pushout choices are exactly the current Route100 choices.

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

Current Route100 nonterminal Fourier branch with only the candidate provider swapped to the coherent closer above.

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

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

Route100 finite surjection count theorem with only the candidate provider swapped to the coherent closer above.