High-contrast homogenization: Provider.Quenched.SmallContrastRestartEndpoint

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

The hcore body from a hatted decay, rather than from a recursion

The endpoint composition reads the recursion and runs the iteration lemma, so its interface is hinit, hsmall, and hrec. The two-stage scheme does not produce a recursion at the restart base: it produces the decay already, in the restart-base decay's shape

∀ n, hatExcess P q N₀' n ≤ Kpre * (3 : ℝ) ^ (-gam * (n : ℝ)) .

hcore_body_of_hatted_decay below is the outer composition read from that shape. Its proof is the endpoint composition's body with the iteration step removed: hhat_all_of_hatted_decay moves the decay to the ∀ n ≥ 2N₀ form that exists_annealed_decay_of_hhat_and_transfer consumes, and the composition is unchanged.

Both lemmas are reindexings of a given decay bound.

theorem HCPolySupport.HighContrast.Quenched.hhat_all_of_hatted_decay {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} {N₀ : ℕ} {Kpre gam : ℝ} (hKpre : 0 ≤ Kpre) (hgam0 : 0 < gam) (hdecay : ∀ (n : ℕ), hatExcess P q N₀ n ≤ Kpre * 3 ^ (-gam * ↑n)) (n : ℕ) : 2 * N₀ ≤ n → 9 / 2 * (↑d * (adaptedHattedContrast P q ↑n - 1)) ≤ 9 / 2 * Kpre * Real.rpow 3 (-gam * ↑(n - 2 * N₀))

The hatted decay past 2N₀, from a decay at the base. The literal hhat hypothesis of exists_annealed_decay_of_hhat_and_transfer, read off a geometric bound on the hatted excess rather than off a recursion.

theorem HCPolySupport.HighContrast.Quenched.hcore_body_of_hatted_decay {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} {N₀ : ℕ} {Kpre gam : ℝ} (hKpre : 0 ≤ Kpre) (hgam0 : 0 < gam) (hgam1 : gam ≤ 1) (hdecay : ∀ (n : ℕ), hatExcess P q N₀ n ≤ Kpre * 3 ^ (-gam * ↑n)) {base Centry Cpref : ℝ} (hbase : 3 ≤ base) (hCpref : 0 ≤ Cpref) (hentry : 3 ^ (2 * N₀) ≤ base.rpow Centry) (hpref : 9 / 2 * Kpre * (Real.rpow 3 (gam / 2) + 1) ≤ base.rpow Cpref) (htransfer : ∀ (m : ℕ), 2 * N₀ ≤ m → annealedContrast P ↑m - 1 ≤ 9 / 2 * (↑d * (adaptedHattedContrast P q ↑(Prop42Scalar.correctedTiltScale N₀ m) - 1)) + 9 / 2 * Kpre * Real.rpow 3 (-↑(m - Prop42Scalar.correctedTiltScale N₀ m))) : ∃ (m₀ : ℕ), 3 ^ m₀ ≤ base.rpow (Centry + (1 + Cpref / (gam / 2))) ∧ ∀ (j : ℕ), annealedContrast P ↑(m₀ + j) - 1 ≤ Real.rpow 3 (-(gam / 2) * ↑j)

The hcore body from a hatted decay. The endpoint composition's conclusion, with the decay supplied rather than derived — the interface the two-stage scheme delivers at the restart base.