High-contrast homogenization: Entry.Multiscale.Global.RunStepsChange #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The change-of-geometry steps of the run #
R3b (Alternative 2, 𝔪₊ ≠ 𝔪⋆) and R3c (Alternative 2, 𝔪₊ = 𝔪⋆ with a failed
determinant test) are the two clauses of SelectionData.Selects that move the metric. Each
produces a successor run state on the updated metric and a strict decrease of the run gauge by
c, the charge and the 2aC(h+2)log(1+δ) jump of the metric being paid out of the
determinant reserve by the shared bookkeeping run_gauge_step. These are the
change-of-geometry alternatives of p.global.selection.
(R3b) Alternative 2, change of geometry with 𝔪₊ ≠ 𝔪⋆ (SelectionData.lean,
p.global.selection). One counted step contains the change and the following
length-h start-up step, so the target is partial_change_decrease
(PotentialDecreases.lean). Its premises: hcomp is the first branch of
comparison_choice's min (ε/2) (Cσ/4) at δ = √ε σ (supplied by the ε chosen in
global_run_of_gap, passed here as hcomp); hw is weight_choice_ge_d; hmet is
partial_change_metric (PartialChangeMetric.lean), whose hsym/hpos/hsymP/
hposP are Recurrence.isSymmetricBlockMat_adaptedMean + run_adaptedMean_blockPosDef, whose
hmono is the
annealed order, whose hbr₁/hbr₂ are the bridge sandwich at δ = √ε σ
(Entry.successful_short_bridge; passed here as hbr₁/hbr₂), and whose hfar is the
case hypothesis hne; hxP1 is the tail clause honeP; hspan is the Alt-1 start-up
clause of Selects applied at the new state (𝔪₊, n+L, n+L), weakened from
C(x + e^{QΔ} − 1) to C·h·(x + e^{QΔ} − 1) using 1 ≤ S.h; the nonnegativities are tree
facts. run_reserve_change pays the charge and the 2aC(h+2)log(1+δ) jump out of the
reserve (run_energy_transfer with J = 2d(h+2)log(1+δ)).
The step carries one hypothesis beyond the printed statement:
haQ : 4 * bigQ d γ * max 1 C ≤ a * C / d, the third conjunct of weight_choice_ge_d.
The proof uses it to apply partial_change_decrease.
(R3c) Alternative 2, 𝔪₊ = 𝔪⋆, failed test (p.global.selection). The
target is failed_test_decrease (PotentialDecreases.lean). hcomp is the second
branch of comparison_choice (≤ Cσ/4); hmet is the bridge half of
partial_change_metric at the reached target (d_pr(𝔪₊, m(𝐀_{n+L,q₊})) ≤ ½log((1+δ)/(1−δ))
from explicitCanonicalMetric_projectiveDistance_le_of_deltaSandwich and hbr₁/hbr₂); hΔ' is
the
negated stop test through det_bridge_not_lt; hspan is conjunct 8 of
fixed_geometry_one_grid_propagation_full at h := 2 * bigQ d γ (premise by rfl),
L := (H : ℤ), guard branch m = n (here k' = n'), with 1 ≤ (H : ℤ) from 4 ≤ H —
this branch has no S.h dependence. run_reserve_change again pays the charge.
The step carries two hypotheses beyond the printed statement:
haQ : 4 * bigQ d γ * max 1 C ≤ a * C / d (the third conjunct of weight_choice_ge_d) and
hspan, the conjunct-8 instance of fixed_geometry_one_grid_propagation_full spelled at the
statement's own C — the theorem Skolemizes its own constant, so the instance cannot be built
from hsrc/hC.