High-contrast homogenization: Entry.Multiscale.Global.RunResidue

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

The residue of the run assembly

GlobalRunGapObligation is everything in the global selection run below the two constant choices: for every horizon H and scale σ it asks for a positive profile constant and a positive lower scale budget such that every coefficient law with the dagger ellipticity and every admissible jStar satisfies the SelectedOutput estimate. Its discharge global_run_residue produces the constant CS of comparison_choice and the source constant Csrc, and hands each consumer the source threshold at every constant at most Csrc. This is the residue of the run that establishes Proposition p.global.selection, and through that proposition it is part of the assembly of Theorem t.polynomial.entry. The assembly of global_run from it is in HCPoly.Entry.Multiscale.Global.RunAssembly; the two Selects projections the run needs and the per-step case analysis run_step_any are in HCPoly.Entry.Multiscale.Global.RunStepAny.

§3 The residue of global_run_of_gap below the constant choices

def HCPolySupport.HighContrast.Multiscale.GlobalRunGapObligation (d : ℕ) (γ : ℝ) (S : SelectionData) (ε Csrc : ℝ) : Prop

Everything in global_run_of_gap downstream of the choice of ε by comparison_choice and of the source constant Csrc, as ONE named obligation. Its user is handed, at every consumer, the discharged source threshold for EVERY constant ≤ Csrc.

Equations

• One or more equations did not get rendered due to their size.

Scalar inputs of the assembly

theorem HCPolySupport.HighContrast.Multiscale.global_run_residue (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (hh : 2 * bigQ d γ ≤ S.h) (hL : ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → 1 ≤ S.L ε σ) : ∃ (CS : ℝ), 1 ≤ CS ∧ ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ε ∈ Set.Ioc 0 S.eps0, (∀ σ ∈ Set.Ioc 0 ε, 1 / 2 * Real.log ((1 + √ε * σ) / (1 - √ε * σ)) + 2 * CS * (↑S.h + 2) * Real.log (1 + √ε * σ) ≤ min (ε / 2) (CS * σ / 4)) → GlobalRunGapObligation d γ S ε Csrc

The run, assembled. The residue of global_run_of_gap: the constants CS (for comparison_choice) and Csrc are produced here, because both are maxima over Skolem constants of hS, initial_provider_input, Entry.fixed_geometry_one_grid_propagation_full and Entry.successful_short_bridge, which only this proof can name.

Route, given H, then σ, then the law and jStar:

1. initial_provider_input produces the entry generation n₀ and the initial sandwich; Geometry.explicitRoundedGrid_one identifies its grid 𝒬(Id) with Id, so its output profile P γ (1 : Mat d) … is run_initial's `profile P γ (Geometry.explicitRoundedGrid jStar
   1. …`.
2. C := max of the weight_choice_ge_d, scales_arith, eccentricity_arith and containment_arith constants (the last at its free real argument d := 4d); Cprof from run_output_profile at Cout := C_S; J := ⌈C₁ logb 3 (2+Π)⌉₊.
3. run_initial (potential) and run_initial_reserve (reserve; its binder hjn₀ : (jStar : ℤ) ≤ n₀ comes from hn₀) bound runGauge at step 0 by c * J.
4. run_step_any supplies the hcont and hstep binders of run_exists_stop.
5. run_exists_stop produces the stopping state, and run_stop_output turns it into SelectedOutput. Every source threshold is the bound ⌈C' * Real.logb 3 (2 * K)⌉ ≤ (jStar : ℤ) at a constant 0 < C' ≤ Csrc.