OneStepDatumPriceOdd #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Pricing the odd-class defect: the split, the reduction, and the refutation #
OneStepBoundaryOdd compresses the boundary branch's whole datum contribution
into the single scalar oddClassDefect x m n V c A recorded as its residue the
pricing
oddClassDefect x m n V c A ≤ C(d) · (3^{n-2})^{3/2} · [∇h]_{C^{0,1/2}(U₂)} ,
read as the manuscript's second boundary-Schauder leg. This module settles the shape of that residue.
1. The universally quantified reading is refuted #
oddClassDefect x m n V c A is stated for an arbitrary odd affine datum
(c,A) ∈ 𝕃_odd. At the zero competitor the defect is exactly the seminorm of
that datum (oddClassDefect_zero_competitor), so on any window carrying the
affine nondegeneracy the defect is strictly positive for every nonzero odd
affine datum (oddClassDefect_zero_competitor_pos) — while the datum side of the
pricing may be 0 (take h ≡ 0; note that hVodd already forces a continuous
competitor to vanish on the met face, so h ≡ 0 on the face is the compatible
datum, not an extra assumption). The pricing therefore cannot hold for an
arbitrary member of the odd class: it must be read existentially, at the best
odd affine datum, exactly as the manuscript's min over 𝕃_odd does.
2. The best odd datum: the split at the met face #
At a single met face {yᵢ = a} the odd class is the line ℝ·(yᵢ − a)
(OddReflectionMap.slope_eq_zero_of_ne_of_meets). The canonical odd affine
datum attached to (c,A) is therefore its normal part Aᵢ·(yᵢ − a)
(oddAffineIntercept, oddAffineSlope), and the complement — the even part
evenAffineIntercept, evenAffineSlope — has vanishing i-slope
(evenAffineSlope_apply_self), i.e. it is constant along the reflection.
oddClassDefect_oddPart_le prices the defect at the odd part of any affine
datum by that datum's own excess gap plus the seminorm of the even part; at an
affine minimizer the gap vanishes and the reduction is exact:
oddClassDefect x m n V (odd part of ℓ*) ≤ ‖even part of ℓ*‖_{L²(U₂)} .
3. The exact remaining inequality (reported, not proved) #
Let V be odd about the met face and harmonic on the doubled window, and let
ℓ* be an affine minimizer of V on U₂. What remains is
‖even part of ℓ*‖_{L²(U₂)} ≤ C(d) · affineExcessRaw U₂ V . (★)
Both sides are L²(U₂) quantities of the same homogeneity in V, and neither
mentions h; (★) is exactly the statement that odd harmonic functions cannot
approximate a nonzero even affine function on the half-box better than a fixed
fraction. It is true — a competitor odd about the face vanishes there, while an
even affine function does not, and harmonicity across the face (the doubled
window puts the face in the interior) caps the transition rate at the window
scale, so the near-face slab already costs a fixed fraction of ‖even part‖.
Its formalization needs interior gradient estimates for harmonic functions at
the face together with a reverse-Chebyshev bound for affine functions, and is
not attempted here.
(★) prices the defect by the excess itself, not by [∇h]. That is the
architectural finding of this module: under hVodd the competitor vanishes on
the met face, i.e. the datum has already been subtracted, so the manuscript's
[∇h]_{C^{0,1/2}(U₂)} leg cannot enter through oddClassDefect; it belongs to
the (still missing) reduction from the true competitor v = h on ∂□_m to an
odd one.
1. The odd/even split of an affine datum at a met upper face #
The intercept of the normal part Aᵢ·(yᵢ − a) of the affine datum
(c,A) at the met upper i-face {yᵢ = a}, a = (1/2)·3^m, in the
affineLift parametrization.
Equations
Instances For
The slope of the normal part: A with every tangential coordinate erased.
Equations
Instances For
The slope of the even part: A minus its normal part.
Equations
Instances For
The intercept of the even part, in the affineEval parametrization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The even part is constant along the reflection: its normal slope vanishes.
The normal part pairs with a vector through its i-coordinate only.
The normal part is the affine function Aᵢ·(yᵢ − a).
The normal part lies in the odd class. In the one-met-face regime the
canonical odd affine datum attached to (c,A) is admissible for
OneStepBoundaryOdd.
2. The reduction: the defect at the normal part #
The affine datum splits: ℓ = (normal part) + (even part), pointwise.
The reduction. The defect at the normal part of an affine datum is at most that datum's own gap to the excess minimum plus the seminorm of the even part.
The reduction at a minimizer. If (c,A) attains the excess minimum on
U₂, the defect at its normal part is at most the seminorm of its even part.
This is the exact residue: what remains's is the bound of the right side by
C(d) · affineExcessRaw U₂ V.