Candidate/target Route135 Section 8 closers

This sidecar leaves all routed/public files untouched. It keeps the Route135 Section 7 provider choices from IntegratedCurrentRouteProofs135WorkerCombined and replaces only the Section 8 candidate/target hooks:

• candidate current semantic packets are routed through CandidateRoute126Closers, replacing the two current semantic leaves by the Route115 scalar/Frattini packets;
• the target Route21 bridge is routed through TargetKmodRRoute22ActualProofs, replacing the two Route21 residual leaves by canonical Y/K ~= B.C and canonical representative-action packets.

Candidate Route135 replacements

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

Route135 candidate replacement for centralCover_candidateMiddleScalarObstructionEvaluatorData, lowered to the Route115 scalar pushout value/linearity packets.

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

Route135 candidate replacement for centralCover_candidateFrattiniAffineFiberCoordinateData, lowered to the Route115 Frattini coordinate/realization/inverse packets.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateTargetRoute135Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Route135 candidate lift-partition provider through the Route126 lowering.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_candidateTargetRoute135Audit {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutValueData B D.tower) × (_ : CentralCoverCandidateMiddleScalarPushoutLinearityData V) × (O : CentralCoverCandidateMiddleRLiftObstructionMapData B D.tower) × (C : CentralCoverCandidateFrattiniLiftCoordinateData B D.tower O) × (R : CentralCoverCandidateFrattiniRealizationData B D.tower O) × CentralCoverCandidateFrattiniCoordinateInverseData C R × CentralCoverCandidateLiftPartitionData B)

Audit surface exposing the lower candidate packets used by the Route135 candidate provider.

Target Route135 replacements

theorem Q2Presentation.Induction.centralCover_targetRoute21LowerProjectionBridgeData_from_candidateTargetRoute135Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21LowerProjectionBridgeData B D)

Route135 target replacement for the Route21 lower-projection residual, lowered to Route22's canonical lower-action equivalence.

theorem Q2Presentation.Induction.centralCover_targetRoute21RepresentativeActionData_from_candidateTargetRoute135Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21RepresentativeActionData B D (TargetKmodRRoute22ActualProofs.route21LowerProjectionBridgeData_of_route22LowerActionEquiv B D E))

Route135 target replacement for the Route21 representative-action residual on the canonical Route22-induced lower projection.

theorem Q2Presentation.Induction.centralCover_targetRoute21ActualBridgeData_candidateTargetRoute135Audit {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) × TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D (TargetKmodRRoute22ActualProofs.canonicalLowerProjectionData_of_route22LowerActionEquiv B D E) × TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21ActualBridgeData B D)

Audit surface exposing Route22's canonical target packets together with the Route21 bridge packet they construct.

theorem Q2Presentation.Induction.centralCover_targetDecorationKernelData_from_candidateTargetRoute135Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetDecorationKernelData B D)

Route135 target decoration-kernel provider through the Route22 lowering.

Route-context integration

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated135_candidateTargetClosers {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_currentIntegrated135_candidateTargetClosers (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

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

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