High-contrast homogenization: Provider.Quenched.SmallContrastAdaptiveDepthGate

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

The adaptive-depth gate: the family clause excludes the echo witness

The the stated witness is admissible for the FIXED-index construction. The family hypothesis at level-adapted lag supplies the recursion clause at every within-octave pair (n, m); on a plateau the drop history collapses (the drop history is constant on a plateau), so once the memory has expired (A·ra^{n−b}·δ₀ ≤ λ/4), the level is small (A·λ ≤ 1/4, automatic from A·δ₀ ≤ 1/2 by the echo-tower quarter bound), and the adapted-lag source is small (s ≤ λ/4), the clause forces λ ≤ (3/4)·λ — false. So the witness VIOLATES the family clause at the middle generations of any sufficiently long octave: the tower profile survives the fixed-index construction only, and the condition's mechanism is not blocked by the corresponding clause.

theorem HCPolySupport.HighContrast.Quenched.iterationDropSum_succ (ra : ℝ) (F : ℕ → ℝ) (n : ℕ) : iterationDropSum ra F (n + 1) = ra * iterationDropSum ra F n + (F n - F (n + 1))

The drop-history recurrence: one step appends the newest drop.

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

The weighted drop history is at most the total drop.