ZDensityLeg #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Z^{(2)} leg: the bad-density random scale and its geometric tail #
ABK26, §4.2. The chain is:
- The
θ-instantiation. The proportion anchorAlgsuperdiff.Frozen.Section4.proportion_of_good_scalesis consumed atθ = δ,ep = s√δ,m₀ = m − j,Mw = j. - The centre-uniform upgrade. The per-centre mass is centre-independent
by the proved translation identities (
Provider.GoodEvents), so each centre of3^{n−1}ℤ^d ∩ □_mcarries the origin's bound; the union over centres uses the explicit enumerationProvider.Proportion.latticeCubeFinset(the count3^{d(j+2)}) andlt_iSup_iff. Neither the cardinality bound nor the covering property is a hypothesis anywhere in this file: both are theorems (card_latticeCubeFinset_le,exists_center_of_badDensity). - The geometric closure.
Algsuperdiff.Probability.WindowTailsturns the per-window bound into the tail ofminimalScale, at the frozen prefactor-tail shapeC exp(−(N−1) s⁹ c⋆² δ² /(Cγ)).
The s-exponent #
The centre union bound converges only when the per-centre rate beats the centre count, i.e. only when
c⋆² s⁹ δ² / γ ≥ K(d) (K(d) ≈ 4 d log 3),
equivalently γ ≤ K(d)⁻¹ c⋆² s⁹ δ². The θ-instantiation itself (step 1)
closes at s⁸ — see measure_center_density_le, whose regime hypothesis is
the printed one verbatim. It is step 2 that needs s⁹. Accordingly every
public of this file downstream of the union bound carries the regime clause at
s⁹, i.e. the printed clause with the single numeral 8 replaced by 9; this
is the ONLY deviation from the printed hypotheses and it is stated at each
site. The manuscript itself uses the matching condition at its own exponent:
it invokes δ ≥ C s^{−7/2} c⋆^{−1} γ^{1/2}, i.e. γ ≤ C^{−2} c⋆² s⁷ δ², which
is e.scale.sep.cond read at the rate exponent s⁷.
Contents #
anchorConst— the proportion anchor's constant, normalised to≥ 1, withanchorConst_spec, the anchor's own conclusion re-run at it.measure_center_density_le— theθ-instantiation: the per-centre bad-density mass at ratec⋆² s⁹ δ² (j+1)/(anchorConst · γ), from the printed regime clause (s⁸).card_centerFinset_le,exists_center_finset_of_badDensity—hcardandhcover, as theorems.zTwoConst— the assembled constant, with its four domination lemmas.measure_tail_badDensity_le— theZ²tail at the frozen prefactor-tail shape.
References #
- ABK26,
p.minimal.scale.separation.sec4. - ABK26,
p.independence.between.scales.
1. Generic window arithmetic #
2. The proportion anchor's constant #
The proportion anchor's constant, normalised to be at least 1. The
anchor's statement is monotone in its constant (both parameter clauses tighten
and the delivered rate weakens as the constant grows), so the normalisation
costs nothing — see anchorConst_spec.
Equations
Instances For
p.independence.between.scales, re-run at anchorConst d. This is the
anchor's own conclusion; the only change is that the constant is anchorConst d ≥ 1.
3. The θ-instantiation: the per-centre bad-density mass #
The per-centre bad-density mass is centre-independent. Both halves of the
stationarity gap are proved: the law-level invariance of
Cutoff.translateCutoffSample and the pointwise observable identity. This is
Provider.GoodEvents.measure_lt_mul_sum_indicator_compl_goodEventAt read at
the two centres y and y'.
The bad-density event at the origin sits inside the anchor's event. The
ℝ≥0∞-valued Cesàro average of the complement indicators exceeding
ofReal delta forces the anchor's ℝ-valued good-proportion to be at most
1 − delta, at base scale m − j and window length j.
The θ-instantiation. The proportion anchor at
θ = δ, ep = s√δ, m₀ = m − j, Mw = j, transported to an arbitrary
centre. The delivered rate is c⋆² s⁹ δ² (j+1)/(anchorConst · γ): the
anchor's s⁷ ep² θ is s⁹ δ² at this instantiation, which is exactly the
s⁹ the frozen tail asserts.
The regime hypothesis is the printed clause, verbatim (exponent s⁸): this
step closes at s⁸. (The union bound over centres does not — see the module
docstring.)
4. The centre enumeration: hcard and hcover, as theorems #
The centre family of the window [m − j, m]: the integer indices of
3^{m−j−1}ℤ^d ∩ □_m, as an explicit Finset (the proved enumeration of
Provider.Proportion).
Equations
Instances For
The centre count of the window [m − j, m] is at most 3^{d(j+2)} ≤ 3^{2d(j+1)}; the exponent 2d is the D of
Algsuperdiff.Probability.count_exp_absorb_const.
A bad density window is witnessed by a centre of the explicit enumeration; the
mechanism is lt_iSup_iff in ℝ≥0∞, so no finiteness and no positivity of δ
is used.
5. The assembled constant #
The Z² leg's constant. Three floor duties, all functions of d alone:
2 · anchorConst d (halving the anchor's rate, which is what pays for the centre
count), 2 · 3^{2d} (the union-bound prefactor against the geometric-summation
constant (1 − e^{−c₀})⁻¹), and log 6 + 4 d log 3 (the anchor's per-window
prefactor 6, and the absorption 2d log 3 + c₀ ≤ c₁).
Equations
Instances For
6. The Z² tail at the frozen prefactor-tail shape #
The geometric tail of the bad-density random scale, at the frozen prefactor-tail shape
P[N ≤ Z²] ≤ C exp(−(N−1) s⁹ c⋆² δ² /(C γ)).
The route: the θ-instantiation measure_center_density_le per centre, the
explicit centre count card_centerFinset_le and cover
exists_center_finset_of_badDensity (both theorems — neither is a binder), then
Algsuperdiff.Probability.windowScale_tail_const_of_center_tails, whose
windowTailConst (2d) c₀ prefactor is absorbed by the (N−1) shift of the
frozen display.
Deviation from the printed hypothesis. The regime clause below is
e.scale.sep.cond with the single numeral 8 replaced by 9 (… s ^ (9 : ℕ)). It is forced: the centre union bound needs the per-centre rate c⋆² s⁹ δ²/(C_a γ) to exceed 2d log 3 + c₀, i.e. it needs γ ≤ K(d)⁻¹ c⋆² s⁹ δ²,
and the printed s⁸ clause is weaker by a factor s, which is a free
parameter with s ↓ 8γ and hence not absorbable into C(d). The
θ-instantiation itself closes at the printed s⁸ — see
measure_center_density_le.