Cover realization parameterized by a block-and-concrete pair

The Route217 realization (centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated217KernelCompact) was parameterized by a MinimalBlockGroupTowerData — an interface carrying the least-form minimal_K field (see PROGRESS.md "SOUNDNESS FINDINGS" #2). Its body, however, uses the group tower only to obtain the pair (B : MinimalBlock p, Dsub : CentralCoverTargetSubgroupConcreteData B).

This file re-houses that body verbatim over the pair itself, so every corrected §7 provider (⊆-minimal kernel, R ≠ 1 branch, 𝒳_R ≠ 0 sub-branch) can drive the same §8 engine without ever producing a least-form tower.

The axioms consumed are exactly the Route217 leaf set on this leg: the Route28 target pair (via TargetKmodRRoute152Closers), the candidate actual pair (via CandidateRoute100CoherentClosers), and the local/CFT lift axioms.

theorem Q2Presentation.Induction.centralCover_realization_of_blockConcreteWithKernel {p : FramedPair} (B : MinimalBlock p) (Dsub : CentralCoverTargetSubgroupConcreteData B) (Hker : CentralCoverTargetDecorationKernelData B Dsub) : Nonempty (CoverRealization B)

Cover realization from a block-and-concrete pair — the (B, Dsub)-parameterized §8 engine (body identical to the Route217 self-group-tower realization), parameterized by the decoration-kernel fact D.Ksub ≤ ker θ_Y (checkpoint-F4: the live §7 branch supplies it from the proven lem:decorationblock Sec7FrattiniTrivialElementaryDecorationProofs.Ksub_le_thetaY_ker, so the Route152 → Route28 residual chain is no longer consumed on the live route).

theorem Q2Presentation.Induction.centralCover_realization_of_blockConcrete {p : FramedPair} (B : MinimalBlock p) (Dsub : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CoverRealization B)

Compatibility wrapper with the original signature: obtains the decoration-kernel fact through the Route152 closers (Route28 residual frontier). Kept for the legacy route files; the live corrected branch uses ...WithKernel with the proven lem:decorationblock fact instead.

theorem Q2Presentation.Induction.fourierBranch_of_blockConcreteWithKernel {p : FramedPair} (B : MinimalBlock p) (Dsub : CentralCoverTargetSubgroupConcreteData B) (Hker : CentralCoverTargetDecorationKernelData B Dsub) : Nonempty (FourierBranchData p)

The Fourier-branch packet from a block-and-concrete pair, parameterized by the decoration-kernel fact (checkpoint-F4).

theorem Q2Presentation.Induction.fourierBranch_of_blockConcrete {p : FramedPair} (B : MinimalBlock p) (Dsub : CentralCoverTargetSubgroupConcreteData B) : Nonempty (FourierBranchData p)

The Fourier-branch packet from a block-and-concrete pair (legacy signature, Route152/Route28 frontier).