OAI/Geometry/RCD/Sobolev/PoissonHarmonicCompactnessConstruction.lean

The actual Poisson/harmonic compactness input

The normalized harmonic sequence determines one classical harmonic model and one subsequence. Every radial mixed-gradient test then converges along that same subsequence by the constructed compact recoveries. The original constant-Laplacian and energy hypotheses are retained in the interface, though only the stated radial gradient and value bounds are needed here.