High-contrast homogenization: Entry.Multiscale.Global.RunStop #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The stop of the run and the stopping argument #
run_stop_output is the Alternative-2 stop (πͺβ = πͺβ, the determinant test succeeds) and
extracts SelectedOutput; run_exists_stop runs the gauge down and produces a stopping
state. Both serve the global selection result p.global.selection. run_exists_stop takes
the per-step alternative hstep and the containment hcont as binders; they are discharged
by run_step_any in HCPoly.Entry.Multiscale.Global.RunAssembly.
The stop configuration of the run at a state: the Alternative-2 stop data, i.e.
exactly the per-state package run_stop_output consumes (beyond the state's own fields and
the scalar binders). Named because it occurs five times β in run_step_any's conclusion, in
run_exists_stop's step hypothesis and conclusion, and in the residue.
Besides the four clauses of the stop predicate (k < n, the smallness
π« + D β€ Ξ·, the fixed point πͺβ = πͺβ and the determinant test), it carries the bridge
sandwich at the retained block and the Alternative-2 output bound at (π¬(πͺβ), n + L).
Those four are produced in the Alternative-2 branch of run_step_any and are not
recoverable from the other four (Alternative 2 and Alternative-3-long are separated by a
guard on which the first four clauses say nothing), which is why they are part of the stop
data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alternative 2, πͺβ = πͺβ, the test succeeds β the stop
(p.global.selection). Retain F = π_{n+2L, q}, s = n+L, t = s+H. The output
fields: symmetry/positivity of F from Recurrence.isSymmetricBlockMat_adaptedMean and
run_adaptedMean_blockPosDef; s < t and t = s + H from 1 β€ H; the two scale bounds
from st.hgen, hnβ and scales_arith; the containment of adaptedCell QF t from
run_entry_containment; the two Loewner bounds are the bridge sandwich hbrβ/hbrβ
transported along heq (explicitCanonicalMetric F = πͺβ = πͺβ, so QF = qβ); the determinant test
is htest; the profile bound is run_output_profile / output_profile_bound fed by the
Alternative-2 transport output houtP and exp_sub_one_le_rpow; the eccentricity output
(βπͺββπͺβ»ΒΉβ)^{1/2} β€ (2+Ξ )^C is eccentricity_arith applied to st.hpr + hpr'.
Generic finite-run scaffolding #
An abstract state space with an index, a gauge and a stop predicate. The run is built by
Nat.rec with classical choice on the successor supplied by the step disjunction, and the
stopping index is extracted with exists_stop_of_potential (FiniteRun.lean) at
charge = 0, Bud = 0.
Iterate the chosen successor map from xβ, with the initial state at iteration zero.
Equations
- HCPolySupport.HighContrast.Multiscale.runIter idx G c xβ i = Nat.rec xβ (fun (x : β) (x_1 : Ξ±) => HCPolySupport.HighContrast.Multiscale.runSucc idx G c x_1) i
Instances For
The run and its stopping step #
The run and its stopping step (p.global.selection). Build
run : β β RunState β¦ by Nat.rec (classical choice) from run_initial: at each step,
apply hS at (run i).m, (run i).k, (run i).n β its premises are the source threshold
βCsrc * Real.logb 3 (2 * K)β β€ (jStar : β€), (run i).hecc, (run i).hone, (run i).hgap,
and run_entry_containment fed by
(run i).hpr, (run i).hgen, hcont β and case-split on the five disjuncts, using
run_step_service, run_step_change, run_step_failed_test, run_step_sync,
run_step_long, with stop i the Alternative-2 case πͺβ = πͺβ whose test succeeds. Then
exists_stop_of_potential (FiniteRun.lean) with
Φ i := runGauge ⦠(run i).m (run i).k (run i).n, charge ①0, Bud := 0, hΦ from
run_potential_nonneg + run_reserve_rounded_nonneg, hstep from the five step cases; the
index bound β(Ξ¦ 0 + 0)/cββ β€ J comes from run_initial + run_initial_reserve and the
choice of J := βCβ Β· logβ(2+Ξ )ββ.