TriangularLattice.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Normalized finite-volume Lipschitz laws on the triangular lattice

This file proves well-definedness of the normalized Lebesgue law in the free coordinates and the almost-sure nonzero-vertex statement. It contains no SLE or GFF convergence theorem and assumes no limiting law, effective stiffness, or tangent-flux coefficient.

abbrev OAI.TriangularSurface.FiniteModel.Free line 28
Source documentation
Coordinates are only the unpinned vertices; Lebesgue measure is on this space, not on the lower-dimensional subset of all-vertex height space.
```
abbrev Free (pins : Set V) := {x : V // x ∉ pins}
```
instance OAI.TriangularSurface.FiniteModel.freeFintype line 30
def OAI.TriangularSurface.FiniteModel.restore line 34
Source documentation
Restore the prescribed boundary values.
```
def restore (pins : Set V) (b : V → ℝ) (h : Free pins → ℝ) (x : V) : ℝ :=
…
```
Mentions: OAI.TriangularSurface.FiniteModel.Free
def OAI.TriangularSurface.FiniteModel.body line 40
Source documentation
The actual unit nearest-neighbor Lipschitz polytope in its free coordinates. The graph and pinned set are arbitrary here; the finite lattice polygon is a special case. Fixed--fixed inequalities are retained.
```
def body (G : SimpleGraph V) (pins : Set V) (b : V → ℝ) : Set (Free pins → ℝ) :=
…
```
Mentions: OAI.TriangularSurface.FiniteModel.Free
def OAI.TriangularSurface.FiniteModel.law line 45
Source documentation
Literal normalized Lebesgue restriction. It is proved to be a probability measure below under the finite-volume model hypotheses.
```
def law [Fintype V] (G : SimpleGraph V) (pins : Set V) (b : V → ℝ) :
    Measure (Free pins → ℝ) :=
…
```
Mentions: OAI.TriangularSurface.FiniteModel.Free
theorem OAI.TriangularSurface.FiniteModel.restore_pin line 49
theorem OAI.TriangularSurface.FiniteModel.restore_free line 53
lemma OAI.TriangularSurface.FiniteModel.continuous_restore line 57
lemma OAI.TriangularSurface.FiniteModel.closed_body line 66
lemma OAI.TriangularSurface.FiniteModel.bound_along_walk line 73
lemma OAI.TriangularSurface.FiniteModel.compact_body line 86
Source documentation
Every vertex has a graph path to a prescribed vertex, exactly the anchoring condition used for boundedness in the source model.
```
lemma compact_body [Fintype V] (G : SimpleGraph V) (pins : Set V)
    (ha : ∀ x : V, ∃ p ∈ pins, G.Reachable x p) (b : V → ℝ) :
    IsCompact (body G pins b) := by
…
```
Mentions: OAI.TriangularSurface.FiniteModel.body
lemma OAI.TriangularSurface.FiniteModel.cube_subset_body line 107
Source documentation
A concrete unit-volume cube lies in the model whenever all fixed heights are at most 1/2 in absolute value. This includes the fixed--fixed edges.
```
lemma cube_subset_body (G : SimpleGraph V) (pins : Set V) (b : V → ℝ)
    (hb : ∀ x ∈ pins, |b x| ≤ 1 / 2) :
    Icc (fun _ : Free pins => -(1 / 2 : ℝ)) (fun _ => 1 / 2) ⊆ body G pins b := by
…
```
Mentions: OAI.TriangularSurface.FiniteModel.Free, OAI.TriangularSurface.FiniteModel.body
lemma OAI.TriangularSurface.FiniteModel.ball_subset_body line 120
lemma OAI.TriangularSurface.FiniteModel.zero_mem_interior line 131
lemma OAI.TriangularSurface.FiniteModel.one_le_volume_body line 137
lemma OAI.TriangularSurface.FiniteModel.law_probability line 149
lemma OAI.TriangularSurface.FiniteModel.ae_mem_body line 159
lemma OAI.TriangularSurface.FiniteModel.ae_free_ne line 166
Source documentation
Coordinate hyperplanes have zero volume, hence no free vertex has a given height with positive probability. This does not assert pointwise tightness as the mesh decreases.
```
lemma ae_free_ne [Fintype V] (G : SimpleGraph V) (pins : Set V) (b : V → ℝ)
    (c : ℝ) : ∀ᵐ h ∂law G pins b, ∀ x : Free pins, h x ≠ c := by
…
```
Mentions: OAI.TriangularSurface.FiniteModel.law, OAI.TriangularSurface.FiniteModel.Free
def OAI.TriangularSurface.FiniteModel.boundaryHeight line 177
Source documentation
The two boundary arcs; vertices in plus get lam, the other pinned vertices get -lam. Membership outside pins has no effect on body or law. Each pinned vertex receives exactly one prescribed value.
```
def boundaryHeight (plus : Set V) (lam : ℝ) (x : V) : ℝ :=
…
```
lemma OAI.TriangularSurface.FiniteModel.abs_boundaryHeight line 180

theorem OAI.TriangularSurface.FiniteModel.finite_model_well_defined line 187

Source documentation

Finite-volume well-definedness of the normalized law. The hypotheses do not contain any limiting, cell, or stochastic identification statement. The normalized law is exactly normalized Lebesgue measure on the polytope.

theorem finite_model_well_defined [Fintype V] (G : SimpleGraph V) (pins plus : Set V)
    (ha : ∀ x : V, ∃ p ∈ pins, G.Reachable x p)
    (lam : ℝ) (hlam : 0 < lam) (hlamhalf : lam ≤ 1 / 2) :
    IsCompact (body G pins (boundaryHeight plus lam)) ∧
    (0 : Free pins → ℝ) ∈ interior (body G pins (boundaryHeight plus lam)) ∧
    0 < volume (body G pins (boundaryHeight plus lam)) ∧
    volume (body G pins (boundaryHeight plus lam)) < ⊤ ∧
    IsProbabilityMeasure (law G pins (boundaryHeight plus lam)) ∧
    (∀ᵐ h ∂law G pins (boundaryHeight plus lam),
      h ∈ body G pins (boundaryHeight plus lam) ∧
      ∀ x : Free pins, h x ≠ 0) := by
…

Mentions: OAI.TriangularSurface.FiniteModel.body, OAI.TriangularSurface.FiniteModel.boundaryHeight, OAI.TriangularSurface.FiniteModel.Free, OAI.TriangularSurface.FiniteModel.law

abbrev OAI.TriangularSurface.Lattice.Vertex line 212
Source documentation
The integer coordinates in the triangular-lattice basis e₁ = (1,0), e₂ = (1/2, sqrt(3)/2).
```
abbrev Vertex := ℤ × ℤ
```
def OAI.TriangularSurface.Lattice.Adj line 215
Source documentation
The six triangular-lattice steps, not square-lattice adjacency.
```
def Adj (x y : Vertex) : Prop :=
…
```
Mentions: OAI.TriangularSurface.Lattice.Vertex
theorem OAI.TriangularSurface.Lattice.adj_symm line 220
theorem OAI.TriangularSurface.Lattice.adj_irrefl line 226
def OAI.TriangularSurface.Lattice.graph line 233
Source documentation
The induced nearest-neighbor graph on the vertices of a finite polygon (or, more generally, any finite set of lattice vertices).
```
def graph (vertices : Finset Vertex) : SimpleGraph vertices where
…
```
Mentions: OAI.TriangularSurface.Lattice.Vertex
def OAI.TriangularSurface.Lattice.embed line 239
Source documentation
The physical embedding at mesh delta.
```
def embed (delta : ℝ) (x : Vertex) : ℝ × ℝ :=
…
```
Mentions: OAI.TriangularSurface.Lattice.Vertex

theorem OAI.TriangularSurface.Lattice.triangular_finite_model_well_defined line 245

Source documentation

The preceding finite-dimensional result specialized to the actual triangular-lattice graph. No assertion about a scaling limit is made.

theorem triangular_finite_model_well_defined (vertices : Finset Vertex)
    (pins plus : Set vertices)
    (ha : ∀ x : vertices, ∃ p ∈ pins, (graph vertices).Reachable x p)
    (lam : ℝ) (hlam : 0 < lam) (hlamhalf : lam ≤ 1 / 2) :
    IsCompact (FiniteModel.body (graph vertices) pins (FiniteModel.boundaryHeight plus lam)) ∧
    (0 : FiniteModel.Free pins → ℝ) ∈
      interior (FiniteModel.body (graph vertices) pins (FiniteModel.boundaryHeight plus lam)) ∧
    0 < volume (FiniteModel.body (graph vertices) pins (FiniteModel.boundaryHeight plus lam)) ∧
    volume (FiniteModel.body (graph vertices) pins (FiniteModel.boundaryHeight plus lam)) < ⊤ ∧
    IsProbabilityMeasure
      (FiniteModel.law (graph vertices) pins (FiniteModel.boundaryHeight plus lam)) ∧
    (∀ᵐ h ∂FiniteModel.law (graph vertices) pins (FiniteModel.boundaryHeight plus lam),
…

Mentions: OAI.TriangularSurface.Lattice.Vertex, OAI.TriangularSurface.Lattice.graph, OAI.TriangularSurface.FiniteModel.body, OAI.TriangularSurface.FiniteModel.boundaryHeight, OAI.TriangularSurface.FiniteModel.Free, OAI.TriangularSurface.FiniteModel.law