High-contrast homogenization: Provider.Quenched.SmallContrastCadenceProfile

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

The cadence profile descent: the scalar family iteration

The profile-head lemma simplifies further: the drop history's head at an anchor is EXACTLY ra^(n−m) · iterationDropSum ra F m (iterationDropSum_split, the semigroup property of the weighted history), so the induction carries the anchors' drop sums as a second inductive component and the profile convergence is one recurrence — no block decomposition.

The margin re-prices from 6A to 24A, with the shares exact: A·ra^(c_A+1) ≤ 1/24 makes the head's collapse share (1/3)·D·θ^i ≤ (1/2)·D·θ^(i+1) at θ = 2A/(2A+1) ≥ 2/3 (equality of the share bound at A = 1), and the error share closes from ra^(c_A+1) ≤ θ/(16A) (again exact at the constants). The result:

F n ≤ (delta + deltaRec) · θ^i          for every n ≥ ns + i·(c_A+1),

— per-stage factor θ = 2A/(2A+1), law-free; stage length c_A + 1, law-free; coefficient delta + deltaRec, Π-polynomial through the trade only; availability ns, linear. This is's linear-threshold preview, delivered by proof, through the profile split, consuming only the family shape and the row-349 dichotomy — no delayed form.

theorem HCPolySupport.HighContrast.Quenched.iterationDropSum_le_total_drop {ra : ℝ} (hra0 : 0 ≤ ra) (hra1 : ra ≤ 1) {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) (m : ℕ) : iterationDropSum ra F m ≤ F 0 - F m

The drop history is at most the total drop.

theorem HCPolySupport.HighContrast.Quenched.iterationDropSum_split (ra : ℝ) (F : ℕ → ℝ) {m n : ℕ} (hmn : m ≤ n) : iterationDropSum ra F n = ra ^ (n - m) * iterationDropSum ra F m + ∑ k ∈ Finset.Ioc m n, ra ^ (n - k) * (F (k - 1) - F k)

The split identity: the weighted drop history factors exactly at any anchor.

theorem HCPolySupport.HighContrast.Quenched.iterationDropSum_anchored {ra : ℝ} (hra0 : 0 ≤ ra) (hra1 : ra ≤ 1) {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {m n : ℕ} (hmn : m ≤ n) : iterationDropSum ra F n ≤ F m - F n + ra ^ (n - m) * iterationDropSum ra F m

The anchored drop-history bound: window telescope plus the exact head.

theorem HCPolySupport.HighContrast.Quenched.cadence_head_margin24 {A alpha : ℝ} {cA : ℕ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hcA : 24 * A ≤ 3 ^ (alpha * ↑cA)) : A * (3 ^ (-alpha)) ^ (cA + 1) ≤ 1 / 24

The 24A margin's attenuation: A·ra^(c_A+1) ≤ 1/24.