EdFinalInputs #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The interior branch's three carried inputs, discharged #
The interior route (EdBridgeInteriorClause) delivers the two-leg one-step
contraction off the harmonic-approximation anchor, but carries three items as
binders:
- the frozen statement's frontier-empty gate on the bare parent image
(z+□_n) ∩ ∂□_m = ∅, together with the one-step's own interior inclusion(x+□_{n-2}) ⊆ □_m; - the harmonic replacement pair
(v, w)on the moved replacement cube, at every scale;
This module discharges all three.
1. The gate, from z ∈ □_{m-1} #
image_add_subset_openCubeSet_of_mem_inner: for z ∈ □_{m-1} and j ≤ m-1
the translated cube z + □_j sits inside □_m — the coordinates satisfy
|z_i| < 3^{m-1}/2 and |w_i| < 3^j/2 ≤ 3^{m-1}/2, so |z_i + w_i| < 3^{m-1} = 3^m/3 < 3^m/2. Since □_m is open it is disjoint from its own frontier, so
the frozen statement's gate follows (inter_frontier_eq_empty_of_subset), and
so does the one-step's interior inclusion (the same lemma at j - 2). This is
exactly the implication disclosed as "the terminal consumer supplies it from z ∈ □_{m-1}", now formalized: the connectedness detour is not needed, the
coordinate computation is direct.
2. The harmonic replacement pair, at every scale #
exists_harmonicReplacementPair: on any open bounded convex nonempty window V and for any
H¹(V) datum Φ there are v : H¹(V) weakly harmonic and w : H¹₀(V) with
v = Φ − w and ∇v = ∇Φ − ∇w (both POINTWISE, as the anchor demands) .
The construction is the proved ResidualCorrectorExistence route run at the
datum's own force +∇Φ (rather than −∇Φ), so that the solution enters with
the sign the anchor's clauses want and both clauses are H1Function.sub_toFun
/ H1Function.sub_grad. Reading the packaged
ResidualCorrectorExistence.exists_weaklyHarmonicOn_of_datum instead would
deliver only the toFun clause: its MemH10 witness is existentially bound,
and pointwise gradient equality does not follow from pointwise value equality.
exists_harmonicReplacementPair_movedCube instantiates it at the anchor's own moved replacement
cube y + □_{n-2}, y = wellPlacedCentre z m (n-2), using the identity
(y + □_{n-2}) = truncatedWindow y m (n-2) (the clamped cube already sits inside □_m).
3. The contraction absorption at the interior ratio #
exists_edFinalStep is EdBridgeFolds.exists_edBridgeStep read on the
interior branch: there is no W' → U_0 re-index there, so the
quasi-monotonicity price κ(d,1) is not paid and the target ratio is θ^k = 3^{-k/4} rather than θ^{k+1}. Both simplifications are strict weakenings of
the proved statement (1 ≤ κ(d,1) and 3^{-(k+1)/4} ≤ 3^{-k/4}), so the
interior step size is the proved k₀(d) unchanged.
References #
- ABK26,
l.harmonic.approximation.good.scales, (the interior clause and its gate);t.regularityStep 4, (the indicator1_{z ∉ □_{m-1}}).
The interior gate, from the printed indicator's own condition. For z ∈ □_{m-1} and
j ≤ m-1 the translated cube z + □_j sits inside □_m.
The frozen interior clause's frontier-empty gate, from any inclusion in □_m: an open
set is disjoint from its own frontier.
The frozen interior clause's gate at the printed indicator's own condition.
2. The harmonic replacement pair #
The harmonic replacement pair exists on every admissible window.
v weakly harmonic, w ∈ H¹₀(V), and BOTH clauses the anchor's interior slot
demands: v = Φ − w and ∇v = ∇Φ − ∇w, pointwise. The Dirichlet solve is run
at the datum's own force +∇Φ, so the pair is (Φ − ρ, ρ) with ρ the
zero-trace solution.
The anchor's moved replacement cube IS a truncated window at the clamped centre.
The harmonic replacement pair at the anchor's own moved replacement cube,
at every scale n with n - 2 ≤ m: the interior route's carried item (c),
discharged from the solution u alone.
3. The contraction absorption at the interior ratio #
1 ≤ κ(d,j) for j ≥ -1: the volume-ratio constant is at least one.
The contraction absorption on the interior branch. There is a step size k₀(d) ≥ 3
beyond which the one-step's contraction prefactor is absorbed into HALF of the iteration
anchor's own ratio θ^k = 3^{-k/4} — no κ(d,1), and no shift to θ^{k+1}, because the
interior clause reads its oscillation on the contraction's own window.