High-contrast homogenization: Provider.Quenched.SmallContrastLinearLedger

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

The linear level schedule at the corrected source model

-(3), first half. At the corrected source model of the strengthened free-threshold estimate — the Π-carrying channel with ABSOLUTE decay at the anchor scale (S1·3^{−bA·m}), a lag-only channel (S0·3^{−b0·lag}, law-free at the instantiation), and an absolute channel at the line scale (S2·3^{−b2·n}) — the squaring level schedule linLam := echoTower (128A²) d0 is VALID with explicitly defined lags, memories, window counts, and pads:

• the S1/S2 burn-ins are paid ONCE, in the start linR 0, and propagate through the pad (linR_abs_cond) — no per-round log₃ S1 (contrast the lag floor of the lag-only model);
• the lag floor carries only log₃ S0 and the level part;
• linear_ledger_descent instantiates the proved the descent induction theorem (the corresponding clause): F n ≤ linLam j from linR j on.

The geometric conversion to hdecay shape is the companion module.

def HCPolySupport.HighContrast.Quenched.linLam (A d0 : ℝ) : ℕ → ℝ

The squaring level schedule.

Equations

• HCPolySupport.HighContrast.Quenched.linLam A d0 = HCPolySupport.HighContrast.Quenched.echoTower (128 * A ^ 2) d0

noncomputable def HCPolySupport.HighContrast.Quenched.linII (A lamj : ℝ) : ℕ

The window count of round j.

Equations

• HCPolySupport.HighContrast.Quenched.linII A lamj = ⌈Real.logb 3 (1 / (16 * A ^ 2 * lamj)) / Real.logb 3 ((2 * A + 1) / (2 * A))⌉₊

noncomputable def HCPolySupport.HighContrast.Quenched.linT (alpha d0 lamj : ℝ) : ℕ

The memory margin of round j.

Equations

• HCPolySupport.HighContrast.Quenched.linT alpha d0 lamj = ⌈Real.logb 3 (d0 / (2 * lamj ^ 2)) / alpha⌉₊

noncomputable def HCPolySupport.HighContrast.Quenched.linL (A b0 S0 lamj : ℝ) : ℕ

The round lag: only the lag-only channel's logarithm and the level.

Equations

• HCPolySupport.HighContrast.Quenched.linL A b0 S0 lamj = ⌈Real.logb 3 (S0 / (2 * A * lamj ^ 2)) / b0⌉₊

noncomputable def HCPolySupport.HighContrast.Quenched.linPad (A bA b2 lamj : ℝ) : ℕ

The absolute-channel pad: keeps the one-time burn-ins propagating.

Equations

• HCPolySupport.HighContrast.Quenched.linPad A bA b2 lamj = ⌈2 * Real.logb 3 (1 / (128 * A ^ 2 * lamj)) / bA⌉₊ + ⌈2 * Real.logb 3 (1 / (128 * A ^ 2 * lamj)) / b2⌉₊

def HCPolySupport.HighContrast.Quenched.linR (ns cA : ℕ) (A alpha b0 bA b2 S0 S1 S2 d0 : ℝ) : ℕ → ℕ

The round starts: the absolute burn-ins are paid once, at the start.

Equations

• One or more equations did not get rendered due to their size.
• HCPolySupport.HighContrast.Quenched.linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0 = ns + ⌈Real.logb 3 (S1 / (A * d0 ^ 2)) / bA⌉₊ + ⌈Real.logb 3 (S2 / (A * d0 ^ 2)) / b2⌉₊

Level facts

theorem HCPolySupport.HighContrast.Quenched.linLam_pos {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (j : ℕ) : 0 < linLam A d0 j

theorem HCPolySupport.HighContrast.Quenched.linLam_le_floor {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (hgs : 128 * A ^ 2 * d0 ≤ 1) (j : ℕ) : linLam A d0 j ≤ d0

theorem HCPolySupport.HighContrast.Quenched.linLam_succ (A d0 : ℝ) (j : ℕ) : linLam A d0 (j + 1) = 128 * A ^ 2 * linLam A d0 j ^ 2

theorem HCPolySupport.HighContrast.Quenched.linR_zero (ns cA : ℕ) (A alpha b0 bA b2 S0 S1 S2 d0 : ℝ) : linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0 = ns + ⌈Real.logb 3 (S1 / (A * d0 ^ 2)) / bA⌉₊ + ⌈Real.logb 3 (S2 / (A * d0 ^ 2)) / b2⌉₊

theorem HCPolySupport.HighContrast.Quenched.linR_succ (ns cA : ℕ) (A alpha b0 bA b2 S0 S1 S2 d0 : ℝ) (j : ℕ) : linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 (j + 1) = linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 j + (max (linL A b0 S0 (linLam A d0 j)) (linT alpha d0 (linLam A d0 j)) + linII A (linLam A d0 j) * (cA + 1) + linPad A bA b2 (linLam A d0 j) + 1)

theorem HCPolySupport.HighContrast.Quenched.ns_le_linR (ns cA : ℕ) (A alpha b0 bA b2 S0 S1 S2 d0 : ℝ) (j : ℕ) : ns ≤ linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 j

The per-round conditions

theorem HCPolySupport.HighContrast.Quenched.linII_spec {A lamj : ℝ} (hA : 1 ≤ A) (hlam : 0 < lamj) : (2 * A / (2 * A + 1)) ^ linII A lamj ≤ 16 * A ^ 2 * lamj

The window count does its job.

theorem HCPolySupport.HighContrast.Quenched.linT_spec {A alpha d0 lamj : ℝ} (halpha : 0 < alpha) (hd0 : 0 < d0) (hlam : 0 < lamj) (hA : 1 ≤ A) : 8 * A ^ 2 * (3 ^ (-alpha)) ^ linT alpha d0 lamj * d0 ≤ 16 * A ^ 2 * lamj ^ 2

The memory margin does its job.

theorem HCPolySupport.HighContrast.Quenched.linL_spec {A b0 S0 lamj : ℝ} (hb0 : 0 < b0) (hS0 : 0 < S0) (hlam : 0 < lamj) (hA : 1 ≤ A) : S0 * 3 ^ (-(b0 * ↑(linL A b0 S0 lamj))) ≤ 2 * A * lamj ^ 2

The lag does its job on the lag-only channel.

theorem HCPolySupport.HighContrast.Quenched.linPad_rpow_le {A bA b2 lamj b : ℝ} (hA : 1 ≤ A) (hlam : 0 < lamj) (hb : 0 < b) (hpadb : 2 * Real.logb 3 (1 / (128 * A ^ 2 * lamj)) / b ≤ ↑(linPad A bA b2 lamj)) : 3 ^ (-(b * ↑(linPad A bA b2 lamj))) ≤ (128 * A ^ 2 * lamj) ^ 2

The pad's rpow value dominates the level-ratio square.

The absolute-channel conditions: paid once, propagated by the pad

theorem HCPolySupport.HighContrast.Quenched.linR_abs_cond {ns cA : ℕ} {A alpha b0 bA b2 S0 S1 S2 d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (hS1 : 1 ≤ S1) (hS2 : 1 ≤ S2) (hbA : 0 < bA) (hb2 : 0 < b2) (j : ℕ) : S1 * 3 ^ (-(bA * ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 j))) ≤ A * linLam A d0 j ^ 2 ∧ S2 * 3 ^ (-(b2 * ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 j))) ≤ A * linLam A d0 j ^ 2

theorem HCPolySupport.HighContrast.Quenched.linear_ledger_descent {A alpha d0 S0 S1 S2 b0 bA b2 : ℝ} {F : ℕ → ℝ} {src : ℕ → ℕ → ℝ} {ns cA : ℕ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hcA : 24 * A ≤ 3 ^ (alpha * ↑cA)) (hd0 : 0 < d0) (hgs : 128 * A ^ 2 * d0 ≤ 1) (hd0small : 9 * A * d0 ≤ 1) (hS0 : 1 ≤ S0) (hS1 : 1 ≤ S1) (hS2 : 1 ≤ S2) (hb0 : 0 < b0) (hbA : 0 < bA) (hb2 : 0 < b2) (hFnn : ∀ (n : ℕ), 0 ≤ F n) (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) (hFd0 : ∀ (n : ℕ), F n ≤ d0) (hfam : ∀ (n m : ℕ), ns ≤ m → m ≤ n → F n ≤ A * iterationDropSum (3 ^ (-alpha)) F n + A * F m ^ 2 + src n m) (hsrc : ∀ (n m : ℕ), ns ≤ m → m ≤ n → src n m ≤ S1 * 3 ^ (-(bA * ↑m)) + S0 * 3 ^ (-(b0 * ↑(n - m))) + S2 * 3 ^ (-(b2 * ↑n))) (j n : ℕ) : linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 j ≤ n → F n ≤ linLam A d0 j

The linear level schedule is valid: the descent holds at it.