High-contrast homogenization: Provider.Quenched.EndpointRelativeParameters

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

Arithmetic of endpoint-relative renormalization windows

The window index is the quotient of the endpoint-relative generation by a fixed stride. Both the recent window and the separation from its annealed reference therefore grow linearly, while the reference generation itself continues to move to infinity.

def HCPolySupport.HighContrast.Quenched.endpointWindowIndex (L n : ℕ) : ℕ

Quotient index of the growing endpoint-relative window.

Equations

• HCPolySupport.HighContrast.Quenched.endpointWindowIndex L n = n / L

def HCPolySupport.HighContrast.Quenched.endpointWindowLength (A L n : ℕ) : ℕ

Recent-window length at generation n.

Equations

• HCPolySupport.HighContrast.Quenched.endpointWindowLength A L n = A * HCPolySupport.HighContrast.Quenched.endpointWindowIndex L n

def HCPolySupport.HighContrast.Quenched.endpointReferenceOffset (A D L n : ℕ) : ℕ

Distance from generation n to its annealed reference generation.

Equations

• HCPolySupport.HighContrast.Quenched.endpointReferenceOffset A D L n = (A + D) * HCPolySupport.HighContrast.Quenched.endpointWindowIndex L n

noncomputable def HCPolySupport.HighContrast.Quenched.endpointTolerance (delta eta : ℝ) (q0 L n : ℕ) : ℝ

Generation-dependent additive tolerance.

Equations

• HCPolySupport.HighContrast.Quenched.endpointTolerance delta eta q0 L n = delta * 3 ^ (-eta * ↑(HCPolySupport.HighContrast.Quenched.endpointWindowIndex L n - q0))

theorem HCPolySupport.HighContrast.Quenched.endpointWindowIndex_mul_stride (L q : ℕ) (hL : 0 < L) : endpointWindowIndex L (L * q) = q

theorem HCPolySupport.HighContrast.Quenched.endpointWindowIndex_mono {L q0 n : ℕ} (hL : 0 < L) (hn : L * q0 ≤ n) : q0 ≤ endpointWindowIndex L n

theorem HCPolySupport.HighContrast.Quenched.endpointReferenceOffset_le {A D L n : ℕ} (hL : L = A + D + 1) : endpointReferenceOffset A D L n ≤ n

theorem HCPolySupport.HighContrast.Quenched.endpointWindowLength_le_referenceOffset (A D L n : ℕ) : endpointWindowLength A L n ≤ endpointReferenceOffset A D L n

theorem HCPolySupport.HighContrast.Quenched.endpoint_reference_generation_ge_index {A D L n : ℕ} (hL : L = A + D + 1) : endpointWindowIndex L n ≤ n - endpointReferenceOffset A D L n

theorem HCPolySupport.HighContrast.Quenched.endpointWindowIndex_sub_lower {L q0 n : ℕ} (hL : 0 < L) (hn : L * q0 ≤ n) : (↑n - ↑(L * q0)) / ↑L - 1 < ↑(endpointWindowIndex L n - q0)

Quotient growth loses at most one stride.

theorem HCPolySupport.HighContrast.Quenched.endpointTolerance_pos {delta eta : ℝ} {q0 L n : ℕ} (hdelta : 0 < delta) : 0 < endpointTolerance delta eta q0 L n

theorem HCPolySupport.HighContrast.Quenched.endpointTolerance_le_delta {delta eta : ℝ} {q0 L n : ℕ} (hdelta : 0 ≤ delta) (heta : 0 ≤ eta) : endpointTolerance delta eta q0 L n ≤ delta

theorem HCPolySupport.HighContrast.Quenched.endpointTolerance_le_generation_decay {delta eta : ℝ} {q0 L n : ℕ} (hdelta : 0 ≤ delta) (heta : 0 < eta) (hL : 0 < L) (hn : L * q0 ≤ n) : endpointTolerance delta eta q0 L n ≤ 3 ^ eta * delta * 3 ^ (-(eta / ↑L) * (↑n - ↑(L * q0)))

Quotient decay implies decay in the physical generation, with one fixed factor lost to integer rounding.

theorem HCPolySupport.HighContrast.Quenched.annealed_error_le_endpointTolerance {delta eta alpha : ℝ} {q0 A D L n : ℕ} (hdelta : 0 ≤ delta) (heta : 0 ≤ eta) (hetaAlpha : eta ≤ alpha) (hL : L = A + D + 1) (hn : L * q0 ≤ n) (hstart : 6 * 3 ^ (-alpha * ↑q0) ≤ delta) : 6 * 3 ^ (-alpha * ↑(n - endpointReferenceOffset A D L n)) ≤ endpointTolerance delta eta q0 L n

Annealed decay at the moving reference generation is absorbed by the generation-dependent tolerance.

theorem HCPolySupport.HighContrast.Quenched.old_cell_burn_le_endpointTolerance {C delta eta gap : ℝ} {q0 A L n : ℕ} (hdelta : 0 ≤ delta) (hetaGap : eta ≤ gap * ↑A) (hL : 0 < L) (hn : L * q0 ≤ n) (hstart : C ≤ delta * 3 ^ (gap * ↑(A * q0))) : C ≤ endpointTolerance delta eta q0 L n * 3 ^ (gap * ↑(endpointWindowLength A L n))

An old-cell calibration at the first family index propagates through the growing window.

theorem HCPolySupport.HighContrast.Quenched.renormBase_endpointTolerance_mono {g nu mu Gain delta eta : ℝ} {q0 A D L n : ℕ} (hdelta : 0 ≤ delta) (hGain : 0 < Gain) (hetaD : eta ≤ mu * ↑D) (hL : 0 < L) (hn : L * q0 ≤ n) : renormBase g nu mu delta Gain (D * q0) 0 ≤ renormBase g nu mu (endpointTolerance delta eta q0 L n) Gain (endpointReferenceOffset A D L n) (endpointWindowLength A L n)

The renormalization base is monotone along the growing family once its separation exponent dominates the tolerance decay.

theorem HCPolySupport.HighContrast.Quenched.rpow_index_growth_le_renormBase_endpoint {g nu mu Gain delta eta : ℝ} {q0 A D L n : ℕ} (hnet : 1 ≤ mu * ↑D - eta) (hL : 0 < L) (hn : L * q0 ≤ n) (hbase : 1 ≤ renormBase g nu mu delta Gain (D * q0) 0) : 3 ^ ↑(endpointWindowIndex L n - q0) ≤ renormBase g nu mu (endpointTolerance delta eta q0 L n) Gain (endpointReferenceOffset A D L n) (endpointWindowLength A L n)

Once the net separation exponent is at least one, the moving renormalization base gains at least one factor of three per quotient step.

theorem HCPolySupport.HighContrast.Quenched.three_pow_affine_index_le {base : ℝ} {q C R : ℕ} (hbase : 3 ≤ base) (hq : 3 ^ ↑q ≤ base ^ 4) : 3 ^ (C * q + R) ≤ base ^ ↑(4 * C + R)

A triadic bracket controls every affine natural generation built from its index, with the constant tail paid by the lower bound 3 ≤ base.

theorem HCPolySupport.HighContrast.Quenched.endpoint_varying_radius_buffer {d A B q0 q : ℕ} {mu baseNow : ℝ} (hA : 1 ≤ A) (hq0 : 1 ≤ q0) (hq : q0 ≤ q) (hmu : 0 < mu) (hB : 1 ≤ B) (hBbase : (2 * ↑A + ↑d * ↑A * Real.log 3) / frGaugeConst d + 1 ≤ 3 ^ (2 * mu * ↑B)) (hbaseGrowth : 3 ^ (↑q - ↑q0) ≤ baseNow) : Real.log (2 * renormCellCount d (A * q)) ≤ frGaugeConst d * (baseNow ^ 2 * 3 ^ (2 * mu * ↑(B * q0)) - 1)

The increasing renormalization base absorbs the cell count of every later window while the radius tail keeps one fixed buffer.