LatticeCharge.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

A combinatorial ray charge and the half-plane argument

We use a half-open cut along the positive horizontal ray: an edge entering height zero from below has charge one exactly when its endpoint has positive first coordinate. This is a combinatorial convention at ray vertices; edges incident to the origin have charge zero. Its restriction to any of the six open lattice half-planes is an exact difference of vertex potentials.

theorem OAI.CoarseAssembly.latticeCharge_self line 20
theorem OAI.CoarseAssembly.latticeCharge_reverse line 24
theorem OAI.CoarseAssembly.latticeCharge_abs_le line 28
inductive OAI.CoarseAssembly.HexDirection line 32
def OAI.CoarseAssembly.HexDirection.eval line 35
def OAI.CoarseAssembly.HexDirection.potential line 43
theorem OAI.CoarseAssembly.HexDirection.adj_bound line 47
theorem OAI.CoarseAssembly.HexDirection.radius_witness line 53
theorem OAI.CoarseAssembly.latticeCharge_halfPlane line 80
Source documentation
Exactness on all six open half-planes is the winding-zero argument, including repeated edges and stationary projections.
```
theorem latticeCharge_halfPlane (d : HexDirection) {u v : LatticeVertex}
    (h : u = v ∨ triangularGraph.Adj u v) (hu : 0 < d.eval u) (hv : 0 < d.eval v) :
    latticeCharge u v = d.potential v - d.potential u := by
…
```
Mentions: OAI.CoarseAssembly.HexDirection, OAI.CoarseAssembly.LatticeVertex, OAI.CoarseAssembly.latticeCharge
theorem OAI.CoarseAssembly.projected_functional_bound line 98
theorem OAI.CoarseAssembly.projected_charge_exact line 113
theorem OAI.CoarseAssembly.charged_walk_meets_halfPlane line 130
Source documentation
A charged closed path must meet the nonpositive side of every one of the six linear functionals.
```
theorem charged_walk_meets_halfPlane (d : HexDirection) {u : V} (p : G.Walk u u)
    (hc : walkCharge (fun u v => latticeCharge (π u) (π v)) p ≠ 0) :
    ∃ w ∈ p.support, d.eval (π w) ≤ 0 := by
…
```
Mentions: OAI.CoarseAssembly.HexDirection, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.latticeCharge
theorem OAI.CoarseAssembly.charged_walk_radius_bound line 139
Source documentation
The geometric estimate in the small-loop lemma.
```
theorem charged_walk_radius_bound {u : V} (p : G.Walk u u)
    (hc : walkCharge (fun u v => latticeCharge (π u) (π v)) p ≠ 0) :
    2 * latticeRadius (π u) ≤ (p.length : ℤ) := by
…
```
Mentions: OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.latticeCharge, OAI.CoarseAssembly.latticeRadius
theorem OAI.CoarseAssembly.charged_walk_all_radius_bound line 153
Source documentation
The same estimate holds at every occurrence of a vertex, by rotating the closed walk. No simplicity hypothesis is needed.
```
theorem charged_walk_all_radius_bound {u : V} (p : G.Walk u u)
    (hc : walkCharge (fun u v => latticeCharge (π u) (π v)) p ≠ 0)
    {w : V} (hw : w ∈ p.support) :
    2 * latticeRadius (π w) ≤ (p.length : ℤ) := by
…
```
Mentions: OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.latticeCharge, OAI.CoarseAssembly.latticeRadius