Theorem 5.15 — the path properties

Proved

QFS.path_props

by dbenbenn · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysismeasure-theoryquadratic-forms-sobolev

For $d \ge 1$ , $0 < \vartheta \le \pi/2$ and any real $R_0$ , there exist $N \ge 1$ , $M \ge 1$ and $\lambda \ge R_0$ such that for every $\vartheta$ -bounded configuration $\Gamma$ there is a family of walks $p_{x,y}$ in the lattice graph of $\Gamma$ , one for each ordered pair of lattice points, with:

(a) $\operatorname{length}(p_{x,y}) \le N$ — one bound for all pairs, with no dependence on $\|x-y\|$ ;
(b) every unordered pair $e$ lies on at most $M$ of the walks, counted over ordered pairs $(x,y)$ ; in particular that collection is finite;
(c) every edge of $p_{x,y}$ has length comparable to the endpoints' separation: $\lambda^{-1}\|x-y\| \le \|u-w\| \le \lambda\|x-y\|$ .

$N$ , $M$ and $\lambda$ are chosen before $\Gamma$ , so they are uniform over all $\vartheta$ -bounded configurations; the family $p$ is chosen after and may depend on $\Gamma$ . Edges join lattice points, at least one of which sees the other inside its own double cone.

Two points of exactness. $R_0$ enters the conclusion only through $R_0 \le \lambda$ — it puts no lower bound on edge lengths. (The development also proves a stronger form, PathPropsLong, which does add $R_0 < \|u - w\|$ on every edge; path_props is the paper's weaker consequence of it.) And on the diagonal, clause (c) forces $\|u-w\| \le \lambda\cdot 0$ , so $p_{x,x}$ must be the empty walk.

Only $\vartheta$ -boundedness is assumed — no measurability of $\Gamma$ .

Preamble

-- Generated by skeleton subtraction from QuadraticFormsSobolev/BlockPaths.lean
-- source: quadratic-forms-sobolev@7a1a680db212
/-
Steps 1 and 2 of the proof of Theorem 5.15: the local path family.

The two steps together produce, at one logarithmic scale and one centre, a walk
in `G` for every admissible pair — the `QFS.ScaleData` that `PathAssembly`
consumes. This file builds the ingredients: the indexing of the majority sets by
`ZMod a`, and the two balanced hashes that choose the scheme's parameters.

*Why hashes.* The paper's `φ_z : A → M` is only required to be balanced
globally, `#φ_z⁻¹(p) ≤ K`. That is not enough for Step 6. A first-jump edge
`{x, q}` is used by every partner `y` of `x` whose assigned walk carries the
index of `q` at `x`'s position along the block walk; the walks with a fixed index
at a fixed position number `a`, so their capacity `K·a` exceeds the `≍ Δ^{nd}`
partners of `x`, and an adversarial balanced `φ_z` may route all of them through
`q`. The multiplicity of that edge is then unbounded.

The repair stays inside the paper's scheme and only fixes its parameters: take
`i = f(y) + g(x)` and `i + j = g(x)`, where `f` and `g` are balanced maps of the
ball to `ZMod a`. The alternating labels are then `α = f(y) + g(x)` and
`β = g(x)`, so

* every consecutive pair `{α, β}` determines both `f(y)` and `g(x)`, bounding an
  interior edge's multiplicity by `#f⁻¹ · #g⁻¹` — this is `cyclic_pair_injective`
  again;
* `α` is, for fixed `x`, a translate of `f` and hence balanced in `y`, which
  bounds the first-jump edge at `x`;
* both `α` and `β` are, for fixed `y`, translates of `g` and hence balanced in
  `x`, which bounds the first-jump edge at `y` — whatever the parity of the block
  walk's length.

The last point is why `α` carries *both* hashes: with `α = f(y)` and `β = g(x)`
an even-length block walk would end on `α`, which is constant in `x`.
-/
import Definitions.Def_QFS_Translate
import Definitions.Def_QFS_Defs
import Definitions.Def_QFS_ConeGap
import Definitions.Def_QFS_RefCones
import Definitions.Def_QFS_Section4
import Definitions.Def_QFS_Cubes
import Definitions.Def_QFS_Section3
import Definitions.Def_QFS_Section5
import Definitions.Def_QFS_Renormalization
import Definitions.Def_QFS_FirstJump
import Definitions.Def_QFS_Assembly
import Definitions.Def_QFS_PathAssembly
import Definitions.Def_QFS_BlockPaths
import Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

open Real Set Metric

open QFS

variable {d : ℕ}

/-! ## Balanced hashes

`exists_fun_fiber_le` with `M = ZMod a` and no constraint on where each element
goes. -/

/-! ## Indexing a majority set by `ZMod a`

The paper writes "WLOG we assume that every majority set contains exactly `a`
different elements" and then treats a block as the tuple `(q^k_i)_{1 ≤ i ≤ a}`.
Formally that is an injection `ZMod a ↪ S`, which exists as soon as `a ≤ #S`. -/

/-! ## The one-point part of admissibility -/

/-! ## What an edge reveals

An edge of the assembled walk is the first jump, the last jump, or an interior
edge of the lift. In each case it pins down enough of `g x` and `f y` for the
multiplicity count. -/

/-! ## The local data of Steps 1 and 2, packaged

Everything the assembly consumes, at one scale `m` and one centre `z`. Each field
is supplied by a result already proved: `walk` by Proposition 5.14 for the choice
graph, `jump` by Lemma 5.16, `rep`/`idx` by `exists_indexed_rep` and the
pigeonhole of Step 2, and `hf`/`hg` by `exists_hash`. -/

/-! ## Step 2: the assembly

For an admissible pair, jump `x` into a block, run the alternating lift of a
block walk with `α = f y + g x` and `β = g x`, and jump out to `y`. -/

/-! ## Block separation

The `sep` field: the cubes of a town have side `ℓ` and centres `h` apart in the
maximum norm, so points of distinct blocks are at distance at least `h − ℓ`. With
`h = Δ^{m+1}` and `ℓ = Δ^m` and `Δ ≥ 2` that is at least `Δ^m`, which is Step 5's
lower bound on an interior edge. -/

/-! ## The retraction `idx`

Blocks at distinct centres are disjoint, so a representative determines its block
and hence its index. -/

/-! ## The number of representatives per block

The paper's `a = Δ^{d(n-1)}/L`, floored at `1` so that it stays positive at the
bottom scale, where the block is a single lattice point and the whole ball holds
only boundedly many points anyway. -/

/-! ## Counting the admissible points

The hashes are balanced because the ball holds only `≍ Δ^{md}` lattice points
while a block's majority set holds `≍ Δ^{md}/L` of them. -/

/-! ## The majority set is large enough to index

The paper's "each block contains at least `Δ^{d(n-1)}/L` lattice points where the
associated cone is favored by majority". -/

/-! ## Steps 1 and 2: the local data exists

Everything is now in place. The constants are the paper's: `Δ` is the scale step
of `ScaleStep`, `R₁` the first-jump radius of Lemma 5.16, `r = 2√d + R₁`, and `R`
the radius Proposition 5.14 returns for that `r`. -/

/-! ## Theorem 5.15

Steps 1–2 (`exists_blockData`), Step 2's assembly (`scaleData_of_blockData`) and
Steps 3–6 (`pathProps_of_scaleData`) compose. The reduction to boundedly many
types is Corollary 2.4: `ref_config_uniform` replaces `Γ` by a configuration with
at most `L` types whose cones sit inside `Γ`'s, and `PathProps.mono_config`
carries the conclusion back. -/

Formal statement

theorem QFS.path_props (hd : 1 ≤ d) {ϑ : ℝ} (hϑ : 0 < ϑ) (hϑ' : ϑ ≤ π / 2) (R₀ : ℝ) :
    PathPropsHolds d ϑ R₀ := by sorry

Source

https://github.com/dbenbenn/quadratic-forms-sobolev/blob/7a1a680db2124d46ce370c91fd450aa454edf491/QuadraticFormsSobolev/BlockPaths.lean#L828-L831

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by dbenbenn · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph