Integrated Route193 concrete: Route192 candidate split plus Route164 target lowering #
This route is the Route192 current sharp lowering route with only the target provider changed to the concrete Route164 projection/action provider.
Compared with
IntegratedCurrentRouteProofs192CandidatePointwiseActualTargetLiteral, it keeps
Route192's two actual candidate §8 leaves through
CandidateRoute192PointwiseActualClosers, keeps the same Route167/175
kernel/pushout providers, and replaces the Route190 target provider by
TargetKmodRRoute164Closers.
The target-side effect is that the integrated finite-count theorem no longer uses the two Route28 atoms
TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28LowerActionEquivData;TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28RepresentativeActionData.
Instead it uses the concrete Route164 projection/action surface:
TargetKmodRRoute164Closers.centralCover_targetRoute164LowerProjectionMapData;TargetKmodRRoute164Closers.centralCover_targetRoute164LowerProjectionSurjectivityData;TargetKmodRRoute164Closers.centralCover_targetRoute164LowerProjectionKernelData;TargetKmodRRoute164Closers.centralCover_targetRoute164RepresentativeActionData.
theorem
Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated193CandidateActualTargetRoute164Lowered
{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_recursive_branch_from_fourier_currentIntegrated193CandidateActualTargetRoute164Lowered
(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_currentIntegrated193CandidateActualTargetRoute164Lowered
(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)