CompetitorVertexData #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The global vertex datum of `l.piecewise.affine.approx` #

This module provides a local vertex-data implementation of Step 1 associated with ABK26's l.piecewise.affine.approx at the level the corrected reading demands: the global assignment of a value to every point of ℝ^d, from which each cell of SW(□_m) reads off its own vertex data, and the two structural clauses of e.hat.linear.properties that assignment satisfies.

The printed construction and the correction it needs #

The manuscript fixes a 2-connected component 𝒞_j of the bad family ℐ and sets, at the vertices V_j of the common coarse mesh of 𝒩(𝒞_j),

ℓ̂_e(v) := ℓ_e(v)              if v ∉ V(𝒞_j) ,
ℓ̂_e(v) := ⨍_{𝒞_j} ℓ_e(x) dx   if v ∈ V(𝒞_j) ,

and does this "one 2-connected component at a time", justified by the assertion that the neighborhoods of distinct components are disjoint. That assertion is false, and there are two admissible constructions: assign the vertex data once on the full simplex complex, or superpose the component corrections while allowing overlap on good cubes.

Throughout, "connected component" is read at the touching relation: badComponent, whose chains join cubes at dist(□,□') = 0 — a strictly finer partition than the one generated by dist ≤ 1 — and the component average is taken over the touching component. That relation is hard-wired (badComponent → BadChain → CubeTouch), so reading the component instead at the scale-covariant relation dist ≤ 3^j would change the datum and require a revisit of this file; the abstract index type I does not insulate against it.

competitorVertexData below is the first construction, implemented at the touching reading above (the datum-level case split is the manuscript's own):

ĝ_p(v) = ⨍_{𝒞(v)} ℓ_p    if v lies in some closed bad cube, 𝒞(v) its component,
ĝ_p(v) = ℓ_p(v)          otherwise.

The two constructions are the same function at the vertex-datum level, and this file proves that rather than assuming it. badComponent_eq_of_mem_closedBall says that if one point lies in two closed bad cubes then those cubes lie in the same component (they touch, so one chain step joins them). Hence at most one component ever claims a vertex, the superposition ℓ_p + Σ_𝒞 (⨍_𝒞 ℓ_p − ℓ_p)·1_{V(𝒞)} has at most one nonzero summand at each point, and no summation, no choice of witness and no disjointness hypothesis is needed. claimedBadComponent is that component, defined without Classical.choose: it collects every bad cube chain-joined to some bad cube whose closed cube contains v.

The active-component reading #

The printed component-local gradient ratio is false under the required overlap-safe construction. The correct form is the sum over the active components 𝒜_R = {𝒞 : R ∈ 𝒩(𝒞)} of diam(𝒞)/ρ_𝒞, optionally followed by a dimension-only overlap count |𝒜_R| ≤ M(d).

Under the single-assignment reading implemented here the deviation at one vertex is governed by the one component that claims it, so what the per-cell estimate needs is a bound valid for every active component -- the hact binder of abs_competitorVertexData_sub_linearFn_le_of_forall_touching, which quantifies over exactly the bad cubes touching the cell's Whitney cube, i.e. over exactly 𝒜_R. Consequently no overlap count is consumed here: card_le_eleven_pow_of_forall_cubeTouch is not used and is not needed for this estimate. It remains the instrument for the superposition presentation, where the corrections genuinely add.

Scope: what this file does NOT do #

It does not build the global piecewise-affine function ℓ̂_p and asserts no continuity, H¹ membership or subordination. Every statement is per-cell: a cell interpolates the global datum at its own vertices (kuhnInterp/kuhnSlope of KuhnInterpolation). Continuity across hanging vertices is the common-coarse-mesh obligation, and e.hat.linear.1 is untouched; both remain open. In sum_of_a_decomp those are carried by the separate binders hF/hG, while hbadF/hoffF are exactly the two clauses proved here.
It asserts no face-to-face property of SW(□_m) and no layer window: no layer, no n_j, no three-layer statement occurs. Nothing here assumes that the neighborhoods of distinct components are disjoint — the point of the construction is that it does not need to.
No slope-square and no collar constant enters.

References #

ABK26: l.piecewise.affine.approx and e.hat.linear.properties (the Step-1 construction and the two structural clauses it must satisfy); the disjointness claim for the neighborhoods of distinct components; the Step-2 vertex bound; and the definitions of ℐ, 𝒩(𝒥), the components, and ℓ_e(x) = e·x.

CompetitorVertexData #

The global vertex datum of l.piecewise.affine.approx #

The printed construction and the correction it needs #

The active-component reading #

Scope: what this file does NOT do #

References #

The ℓ¹ size of a slope #

The component that claims a point #

The component average ⨍_{𝒞} ℓ_p #

The global vertex datum #

Vertices of a cell of a Whitney cube #

Clause 1 of e.hat.linear.properties #

The Step-2 vertex bound #

The global vertex datum of `l.piecewise.affine.approx` #

The `ℓ¹` size of a slope #

The component average `⨍_{𝒞} ℓ_p` #

Clause 1 of `e.hat.linear.properties` #