SuperposedDivergence #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
∇·D̂_q at the superposed competitor (the G-leg of the superposed branch) #
CollarLayerEnvelopeG.lean builds the manuscript's antisymmetric matrix D̂_q
(e.hatdq) and its cell divergence ∇·D̂_q(𝔰) at the single-mesh
competitor family ℓ̂_p = competitorVertexData ℐ p. This module runs the
same construction on the superposed family ℓ̂_p = ℓ_p + Σ_𝒞 (ℓ̂_p^𝒞 − ℓ_p), the second of the two admissible constructions, and provides the
following local G-leg objects and estimates:
- the field
superposedCompetitorDivergence— this is∇·D̂_q, the objecte.hat.D.bcspeaks about, and the object whose solenoidality is thehGleg ofMultiscale.sum_of_a_decomp_cutoff; - its cell constants
superposedCompetitorCellDivergence; - the three cell-constant clauses of
e.hat.linear.propertiesat that field (hGc,hbadG,hoffG); and - its collar layer envelope, at
superposedDivConst d = 2 · superposedGradConst d.
Why this module exists (finding M-1) #
The superposed branch of the Step-3 conclusion had used
superposedCompetitorSlope … q — the gradient construction re-run at the
load q — in its G leg. That is the wrong object: the manuscript's G leg
is ∇·D̂_q, the divergence of the antisymmetric matrix built from the d
basis members ℓ̂_{e_i}, not ∇ℓ̂_q. The two agree neither in law nor in
shape, and the solenoidality binder stated at ∇ℓ̂_q is refutable. Everything
below is stated at ∇·D̂_q; nothing below refers to, or corrects, the branch
that used the gradient.
The object #
For the superposed family, e.hatdq reads entrywise
(D̂_q)_{ij} = (d − 1)⁻¹ ( q_j ℓ̂_{e_i} − q_i ℓ̂_{e_j} ) ,
which is superposedCompetitorAntisymEntry: competitorAntisymDatum's formula
with the single-mesh vertex datum replaced by the superposed competitor, so
only the d basis members occur, exactly as printed, and no linearity of p ↦ ℓ̂_p is assumed (e.hat.linear.linearity, is not used).
superposedCompetitorAntisymEntry_antisymm is the antisymmetry.
At the manuscript's divergence convention (∇·A)_j = ∑_i ∂_{x_i} A_{ij} (the
footnote) the j-th coordinate of ∇·D̂_q is the sum over i of the i-th
coordinate of the gradient of the (i,j) entry. The superposed competitor
carries a defined piecewise-constant gradient field
superposedCompetitorSlope (there is no single mesh whose Kuhn-slope operator
applies to the entry — that is exactly what denies), so
superposedCompetitorDivergence is defined by that distributed expression:
(∇·D̂_q)(x)_j = ∑_i (d − 1)⁻¹ ( q_j (∇ℓ̂_{e_i})(x)_i − q_i (∇ℓ̂_{e_j})(x)_i ) .
Two theorems show that this is the proved single-mesh construction and not a new one:
competitorDivergence_eq_sum_entrywise says the distributed expression at
single-mesh Kuhn slopes IS CollarLayerEnvelopeG.competitorDivergence (it is
kuhnSlope_competitorAntisymDatum, i.e. the unconditional linearity of
kuhnSlope in its datum, re-summed), and
globalCompetitorDivergence_eq_competitorDivergence says that at ONE component
— where a single mesh does govern — the distributed expression evaluated on
that component's own field is literally competitorDivergence at the root cell
containing the point.
The normalization ∇·D_q = q #
superposedCompetitorCellDivergence_sub_eq is the exact algebraic identity
(∇·D̂_q)(𝔰)_j − q_j = (d−1)⁻¹ ( (∑_i (u_i)_i) q_j − ∑_i q_i (u_j)_i ) ,
u_i = ∇ℓ̂_{e_i}(𝔰) − e_i ,
the d of ∑_i (e_i)_i and the q_j of ∑_i q_i (e_j)_i cancelling against
the (d−1) of e.dq — this is the display ∇·D_q = q in its cellwise form,
and superposedCompetitorCellDivergence_eq_of_cellSlope_basisVec is that
display itself: on a cell where the superposed basis slopes are the basis
vectors (clause 3 of e.hat.linear.properties, off the collar) the divergence
is exactly q. It is the reason hoffG is a theorem here.
The route to the layer envelope, and the constant #
The (2d−2)²-cancellation core vecNormSq_divergenceDeviation_le of
CollarLayerEnvelopeG is reused verbatim: if every entry of the deviation
family u is at most η, then |(∇·D̂_q)(𝔰) − q|² ≤ (2η)² |q|². What feeds
it here is not the coordinatewise Step-2 estimate of the single-mesh branch (no
single mesh, hence no kuhnSlope-level bound) but the proved summed
active-component envelope, read at the d basis loads:
|∇ℓ̂_{e_i}(𝔰) − e_i|² ≤ superposedGradConst d ² · 3^{2b(k+h_k)} · |e_i|²
(SuperposedEnvelope.badFamily_vecNormSq_superposedCompetitorCellSlope_sub_le_layerEnvelope
at p := basisVec i, with |e_i|² = 1), and a coordinate of a vector is at
most its Euclidean norm, so η = superposedGradConst d · 3^{b(k+h_k)} serves.
The constant, itemized honestly. 2η gives
superposedDivConst d = 2 · superposedGradConst d = 2 · M(d) · 648 d = 3888 d · 11^d ,
i.e. the summed gradient constant times 2, and nothing else. A further factor of order
d · |q|_{ℓ¹} does not appear, for two reasons, both checkable in the proof: (i) the
d entries of the inner sum are priced through the proved local core, whose (d−2)² + 2d(d−2) + d² = (2d−2)² is exactly cancelled by the (d−1)⁻¹ of e.dq, leaving the
factor 2 and not a factor d; and (ii) the ℓ¹ size of the load never enters, because
the deviation bound fed into the core is an ℓ^∞ bound obtained from the Euclidean
envelope at the basis loads (|e_i|_{ℓ¹} = 1), so the ℓ¹ → ℓ² conversion is already
inside superposedGradConst d. The comparison with the single-mesh branch is the
expected one: there the G-leg constant equals the F-leg's 648 d because the F leg
pays an extra d for a general slope p; here the F-leg constant superposedGradConst d already contains that d, so the G leg is 2 × it. Nothing is optimized, and no
random quantity, layer index or component enters the constant.
Scope: what is NOT claimed #
This module is the per-cell estimate and the three cell-constant clauses, only.
- No divergence-freeness.
e.hat.D.bc,∇·D̂_q ∈ q + L²_{sol,0}(□_m), is not proved and is not implied by anything below. is explicit that the parenthetical "(sinceD̂_qis antisymmetric)" carries the whole face-jump argument, and that it works only becauseD̂_q ∈ W^{1,∞}: for the superposition that needs the global continuity of the superposedℓ̂_{e_i}, which needs local finiteness of the component family, whichGlobalSuperposition.leanexplicitly does not supply. ThehGleg of the composition therefore remains an O disclosed binder — but it is now stated at the right object. - No gradient identification.
superposedCompetitorSlope, and hencesuperposedCompetitorDivergence, are defined piecewise-constant fields; nothing identifies either with a distributional gradient or divergence. - No new probabilistic input, no new geometry. The diameter datum, the
window, the multiplicity bound
|𝒜_R| ≤ M(d)and the cluster geometry are consumed only through the proved summed envelope; none is re-derived, and no overlap count occurs below.
References #
- ABK26, (
e.hat.linear.1), (e.hat.linear.linearity), (e.dq), (the divergence-convention footnote), (∇·D_q = q), (e.hatdq), (e.hat.D.bc), (the cell-constant values), (l.piecewise.affine.approx,e.hat.linear.properties; clause 1, clause 3), (Step 2), (r.gradient.bound.simplified), (e.bounds.on.slopes.when.bad). - That is the factor
d²the proved local core removes.
e.hatdq at the superposed family #
∇·D̂_q at the superposed family, at the manuscript's divergence
convention (∇·A)_j = ∑_i ∂_{x_i} A_{ij} (the footnote): the sum over i of
the i-th coordinate of the gradient of the (i,j) entry, at the
superposition's own defined gradient field.
This is the field whose solenoidality is e.hat.D.bc; that statement is NOT
proved here (see the module Scope).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constant value ∇·D̂_q(𝔰) on a cell, read at the cell's interior point
exactly as superposedCompetitorCellSlope is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The deviation identity and ∇·D_q = q #
The deviation identity, as pure algebra on a family of cell slopes. For
any family S of vectors (the roles: S i = ∇ℓ̂_{e_i}(𝔰)),
(∑_i (d−1)⁻¹ ( q_j S_i i − q_i S_j i))_j − q_j
= (d−1)⁻¹ ( (∑_i (S_i − e_i)_i) q_j − ∑_i q_i (S_j − e_j)_i ) .
The d produced by ∑_i (e_i)_i and the q_j produced by ∑_i q_i (e_j)_i
cancel against the (d−1) of e.dq; this is the display ∇·D_q = q in its
cellwise form, and it is what makes the left-hand side a deviation.
The deviation identity at the superposed cell divergence (in cellwise
form): with u_i = ∇ℓ̂_{e_i}(𝔰) − e_i,
(∇·D̂_q)(𝔰) − q = (d−1)⁻¹ ( (∑_i (u_i)_i) q − (u_·ᵀ q) ) .
∇·D_q = q (the display), cellwise: on a cell where the superposed basis
slopes are the basis vectors themselves — the situation of clause 3 of
e.hat.linear.properties off the collar — the divergence of D̂_q is exactly
q. This is the normalization that makes the deviation identity a statement
about a deviation, and it is the reason hoffG below is a theorem.
The three cell-constant clauses at ∇·D̂_q #
The G-half of the sum_of_a_decomp clauses at ∇·D̂_q, at one cell.
- the field is constant on the open cell — every basis slope is
(
e.hat.linear.propertiesclause on the superposition), and∇·D̂_qis built from those pointwise; - the constant is
0when the cell's Whitney cube is bad: every basis slope is0there (clause 1), so every entry ofD̂_qhas zero gradient; - the constant is
qwhen the cube lies off𝒩(ℐ): every basis slope ise_ithere (clause 3), and the normalization∇·D_q = qapplies.
Only the proved superposition clauses are used; no disjointness of collars, no overlap count and no finiteness of the component family enters.
Over the subtype ↥(simplexPartition m hn) these are literally the hGc,
hbadG and hoffG hypotheses of Multiscale.sum_of_a_decomp_cutoff.
The collar layer envelope of ∇·D̂_q #
The collar gradient constant of the G leg of the superposed branch, 2 · superposedGradConst d = 3888 d · 11^d: the summed active-component constant
times the factor 2 produced by the (2d−2)² cancellation of e.dq. It is
the Cgrad of r.gradient.bound.simplified for ∇·D̂_q at the superposed
competitor.
Equations
Instances For
The collar layer envelope of ∇·D̂_q at the superposed competitor: on
every cell of every layer-k Whitney cube
|(∇·D̂_q)(𝔰) − q|² ≤ (2 · superposedGradConst d)² · 3^{2 b (k + h_k)} · |q|² .
The route follows the proved single-mesh one at the superposed input: the
proved summed active-component envelope at each of the d basis loads e_i
bounds every coordinate of u_i = ∇ℓ̂_{e_i}(𝔰) − e_i by η = superposedGradConst d · 3^{b(k+h_k)} (a coordinate is at most the Euclidean
length, and |e_i|² = 1), and CollarLayerEnvelopeG's
vecNormSq_divergenceDeviation_le turns that into (2η)²|q|², the (2d−2)²
of the d − 1 surviving terms being cancelled by the (d−1)⁻¹ of e.dq.
As in the F leg nothing on the right depends on a component, on a layer of a
component or on the sample: the whole random content is in havoid.