OneStepOddClassCorner #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The corner pricing of the odd-class defect #
's residue (2). At two met faces the odd affine class collapses to {0}
(affineLift_eq_zero_of_two_met), so the odd-class defect of the boundary
producer degenerates to ‖V‖_{L²(U₂)} − E_raw(U₂,V) and the proved one-face
pricing (★) does not apply. This module proves the corner pricing:
‖V‖_{L²(U₂)} ≤ C(d) · E_raw(U₂, V) (★★)
for V classically harmonic on the doubled window, odd under every
met-face reflection, at a window meeting the upper faces of two distinct
coordinates i ≠ j (the remaining met set arbitrary); and hence
oddClassDefect x m n V 0 0 ≤ C(d) · E_raw(U₂, V) ,
the exact leg shape the proved K-package consumers carry at the corner datum
(c, A) = (0, 0) — the only member of the collapsed class.
The mechanism #
Let ℓ* be an affine minimizer and f = V − ℓ*, E = ‖f‖_{L²(U₂)},
P = ‖ℓ*‖_{L²(U₂)}. With evenᵢ/evenⱼ the even parts of ℓ* at the two
faces and e_{ij} the doubly even part (= evenⱼ of the affine evenᵢ),
ℓ* = evenᵢ + evenⱼ − e_{ij} ,
and each of the three parts is priced on a window-hugging near-face slab by
the two-point Taylor elimination (abs_evenAffinePart_le_pointwise_of_mem):
the single-face applications at i and at j against the residual f, and
the doubly even part at the face j against the residual V − evenᵢ on
the corner slab, where the leftover normal ramp oddᵢ = ℓ* − evenᵢ is
pointwise at most |Aᵢ|·delta and hence O(t)-small against
P + ‖evenᵢ‖ by the box-moment lower bound. The Hessian remainders are
O(t²)·‖f‖_{L²(R)}, and ‖f‖_{L²(R)} folds back to (E + P) by the
full-met-set odd fold and the affine moment comparison. Choosing the depth
fraction t = t(d) small absorbs every P-feedback at coefficient < 1,
closing P ≤ C(d)·E.
Scope (disclosed) #
The two active faces are met upper faces, matching every proved convention
of the one-face chain (evenAffinePart, the slab geometry, (★) itself are
stated at upper faces). Lower and mixed corners require either the mechanical
lower-face twins of those atoms or a coordinate-negation transport; neither is
built here, and the composed corner consumption must supply the upper-upper
configuration or its transported image. The met-face oddness binders are the
global pointwise identities, exactly as in the proved (★) and one-face
producer.
1. The slab estimate, box-generic #
The near-face slab estimate, box-generic: the L² size of the even
part on the slab is priced by the residual on the slab, on its inward
translate, and the Hessian remainder.
2. Transfer helpers #
The subset transfer with an explicit ratio bound.
3. The Hessian value on a Taylor set #
The Hessian value. For F harmonic on the doubled window and a set whose
points carry sup-balls of radius 3^k/16 inside it, there is a Hessian bound
M on the set with M·delta² ≤·256·√(32^d)·t²·‖F‖_{L²(R)} at delta = t·3^k.
4. Small instantiation helpers #
The controlled comparison of the window against a window-hugging slab:
κ = 4, active coordinates carried by zero slopes.