High-contrast homogenization: Provider.Quenched.SmallContrastEndpointDataMinimal

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The endpoint's frozen-side data, with the burn-in's own upper bound

This is the half the polynomial burn-in cannot supply on its own.

exists_endpoint_frozen_data_minimal returns the burn-in N1 as an existential and records only sK + 1 ≤ N1. That is everything the account needs and nothing hentry needs: hentry must bound 3 ^ N1 above by a power of the telescope's base, and an existential burn-in admits no upper bound at all.

The repair is the same one applied to the source scale and the gap separately: expose the burn-in's decomposition. N1 = sK + 1 + gap is how exists_bootstrap_smallness_uniform_minimal builds it, and gap comes from the gap existence statement, whose minimal companion exists_gap_three_pow_le_minimal carries the upper bound 3 ^ gap ≤ 3 * max 1 (CB * factor / sigma) at no cost — the same ⌈log₃ ·⌉ witness, one more conclusion.

So this file is a parallel restatement, not new mathematics: the same constant, the same proof, with gap returned beside the data it determines. With it and exists_source_scale_minimal, exists_burnIn_exponent_canonical applies and hentry closes.

theorem HCPolySupport.HighContrast.Quenched.exists_bootstrap_smallness_uniform_minimal (d : ℕ) (hd : 2 ≤ d) (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (CB : ℝ), 0 < CB ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∀ (Cd : ℝ), max 1 (12 * ↑d * √↑d) ≤ Cd → ∀ (sK : ℤ), 0 ≤ sK → growthBar K ≤ 3 ^ sK → ∀ (mAl : Mat d), Matrix.PosDef mAl → ∀ (sigma delta cStar : ℝ), 0 < sigma → ↑d * bootstrapTiltPolynomial sigma (↑d * cStar) ≤ delta → annealedContrast P 0 - 1 ≤ cStar → ∃ (gap : ℤ), 1 ≤ gap ∧ 3 ^ gap ≤ 3 * max 1 (CB * bootstrapAdapterFactor Cd g K E mAl / sigma) ∧ ∀ (lq : ℤ), ↑(kZero d) ≤ lq → ∀ (n : ℤ), sK + 1 + gap ≤ n → hatExcessAt P (roundedGrid lq mAl) n ≤ delta

The bootstrap floor at a minimally chosen gap. The parallel of exists_bootstrap_smallness_uniform_minimal that returns the gap it built the burn-in from, together with the gap's own upper bound.

theorem HCPolySupport.HighContrast.Quenched.exists_endpoint_frozen_data_minimal (d : ℕ) (hd : 2 ≤ d) (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (Csub : ℝ) (CB : ℝ), 0 < Csub ∧ 0 < CB ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∀ (Cd : ℝ), max 1 (12 * ↑d * √↑d) ≤ Cd → ∀ (sK : ℤ), ↑(kZero d) ≤ sK → growthBar K ≤ 3 ^ sK → ∀ (mAl : Mat d), Matrix.PosDef mAl → ∀ (sigma delta cStar : ℝ), 0 < sigma → ↑d * bootstrapTiltPolynomial sigma (↑d * cStar) ≤ delta → annealedContrast P 0 - 1 ≤ cStar → ∃ (gap : ℤ), 1 ≤ gap ∧ 3 ^ gap ≤ 3 * max 1 (CB * bootstrapAdapterFactor Cd g K E mAl / sigma) ∧ ↑(kZero d) ≤ sK + 1 + gap ∧ IsRoundedGrid (sK + 1 + gap) (roundedGrid (sK + 1 + gap) mAl) ∧ (∀ (k : ℤ), sK + 1 + gap ≤ k → hatExcessAt P (roundedGrid (sK + 1 + gap) mAl) k ≤ delta) ∧ ∀ (j' p' : ℤ), sK + 1 + gap ≤ j' → j' ≤ p' → ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid (sK + 1 + gap) mAl) j' w ∈ adaptedCell (roundedGrid (sK + 1 + gap) mAl) p'} ∧ Z.card = 3 ^ (d * (p' - j').toNat) ∧ Z.Nonempty ∧ lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt (roundedGrid (sK + 1 + gap) mAl) j' w) a))) (adaptedMean P (roundedGrid (sK + 1 + gap) mAl) j')) (adaptedMean P (roundedGrid (sK + 1 + gap) mAl) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell (roundedGrid (sK + 1 + gap) mAl) j') a) (adaptedMean P (roundedGrid (sK + 1 + gap) mAl) j')) (adaptedMean P (roundedGrid (sK + 1 + gap) mAl) p')

The endpoint's frozen-side data, with the gap exposed. Identical to exists_endpoint_frozen_data_minimal except that the burn-in is presented as sK + 1 + gap with the gap's upper bound — which is exactly what exists_burnIn_exponent_canonical consumes.