High-contrast homogenization: Entry.Multiscale.Global.RunSteps #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The fixed-geometry steps of the run #
The three fixed-geometry clauses of SelectionData.Selects that keep the metric and the
retained generation (𝔪, k) and advance only n: R3a (Alternative 1, service), R3e
(Alternative 3, synchronized) and R3f (Alternative 3, long). Each turns its propagation
guard into the potential decrease of the matching one-grid estimate and transfers that
decrease, through the determinant reserve, into a drop of c in the run gauge, carrying the
run-state invariants to the successor state. These are the continuing moves of the run whose
stopping output is Proposition p.global.selection, and through that proposition they enter
the assembly of Theorem t.polynomial.entry.
(R3a) Alternative 1, service step (SelectionData.lean). The guard supplies
x > η and the quarter propagation x'@(n+h) ≤ x/4 + C Δ̂;
potential_step_sub_le_of_quarter_bound
(Run.lean) converts it into the potential decrease with the charge
a C / d · Δ̂_h(n), and run_reserve_sync pays that charge out of the reserve, so the
transferred gauge drops by c. The nonnegativities hx' and hΔ are tree facts
(Annealed.logDetLoss_nonneg, profile_add_determinantDrift_nonneg,
logDetLoss_le_synchronizedLogDetLoss). The new state keeps (m, k), so hecc, hm,
hpr transport; hone/hgap are the tail clauses hone'/hgap'; hgen uses
S.h ≤ 2L+H+h.
(R3e) Alternative 3, synchronized (SelectionData.lean). Selects supplies
only the three guards and no propagation clause; the propagation is conjunct 6 of
Entry.fixed_geometry_one_grid_propagation_full instantiated at h := S.h, which needs
hh : 2 * bigQ d γ ≤ S.h (conjunct C1 of Selects), L := 1, n := st.k, m := st.n, with
st.k + S.h ≤ st.n from st.hgap and the source threshold
⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ (jStar : ℤ). Its
shape 1/8·e^{QΔ̂}·x + C(e^{QΔ̂} − 1) is exactly potential_step_sub_le_of_exp_bound.hprop, so
the target here
is potential_step_sub_le_of_exp_bound (Containment.lean), not the quarter variant. The charge
aC/d·Δ̂ is paid by run_reserve_sync. The state transition is as in R3a.
(R3f) Alternative 3, long (SelectionData.lean). Target:
long_step_decrease (Containment.lean). hΔ is the guard through
det_bridge_gt; hx1 : x ≤ 1 is the guard x ≤ S.eta ε σ through
selectionData_eta_le_one; hL : 1 ≤ L is conjunct C2a of Selects, the binder hL1; hw, ha,
hlogH are weight_choice_ge_d; hspan is conjunct 3 (or 8) of
fixed_geometry_one_grid_propagation_full at h := S.h — which needs hh : 2 * bigQ d γ ≤ S.h
(conjunct C1 of Selects: the alternatives only give k + S.h ≤ n, while the supplier's
guard is k + 2 * bigQ d γ ≤ n) — with L := 2 * (S.L ε σ : ℤ). The charge
aC/d·Δ_{n,n+2L} is paid by run_reserve_advance. The state keeps (m, k) and advances
n by 2L.
The binder haQ : 4 * bigQ d γ * max 1 C ≤ a * C / d is the third conjunct of
weight_choice_ge_d.