Import the Apollonian classification of integer superharmonic matrices

LeanPool/ApollonianSuperharmonic.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+module
+
+public import LeanPool.ApollonianSuperharmonic.IntegerSuperharmonicCharacterization
+public import LeanPool.ApollonianSuperharmonic.BandOdometerTheorem
+public import LeanPool.ApollonianSuperharmonic.IntegralityTiling
+public import LeanPool.ApollonianSuperharmonic.LambdaTiling
+public import LeanPool.ApollonianSuperharmonic.BandLatticeEquality
+
+/-!
+# Apollonian classification of integer superharmonic matrices
+
+Source: arxiv:1309.3267, url:https://github.com/wpegden/superharmonic
+Authors: Wesley Pegden
+Status: verified
+Main declarations: `ApollonianSuperharmonic.IntegerSuperharmonicCharacterization`,
+  `ApollonianSuperharmonic.BandOdometerTheorem`, `ApollonianSuperharmonic.IntegralityTiling`,
+  `ApollonianSuperharmonic.LambdaTiling`, `ApollonianSuperharmonic.BandLatticeEquality`
+Tags: apollonian-packings, superharmonic-functions, discrete-potential-theory, lattice-tilings
+MSC: 31C20, 52C15, 60G50
+-/
+
+/-!
+## Upstream formalization
+
+Adapted from Wesley Pegden's Apache-2.0 Trellis formalization at commit
+`45094b210503f117502dec51caf737e96da221f8`. The mathematical source is Levine,
+Pegden and Smart, *The Apollonian structure of integer superharmonic matrices*.
+Trellis produced the Lean proofs using AI agents; the project records `AI` provenance.
+
+The entry module exposes the five headline results. The project also preserves
+explicit Ford and diamond lattice and maximality results, additional odometer
+cocycles, and supporting geometric lemmas from upstream. The upstream paper,
+process tooling and development history are not imported.
+The upstream reference notes explain two local repairs to the printed proof:
+edge-supported interfaces with isolated corners, and occurrence-oriented unit strings.
+The recursive-vector API also retains upstream’s product-compatible initialization,
+whose signs and affine offsets differ from the printed Section 5.3 display.
+`RecursiveVectorSystem` records both triples and the base product-identity discrepancy.
+-/

LeanPool/ApollonianSuperharmonic/AcyclicIndegreeOrientation.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+module
+
+public import Mathlib.Init
+
+public import LeanPool.ApollonianSuperharmonic.FourNeighborAdjacent
+
+-- [TABLET NODE: AcyclicIndegreeOrientation]
+
+/-!
+# AcyclicIndegreeOrientation
+
+Adapted from Wesley Pegden’s Apache-2.0 Trellis formalization of Levine–Pegden–Smart.
+Changes: pool module paths, public exports, project namespace and current Mathlib compatibility.
+-/
+
+@[expose] public section
+
+namespace ApollonianSuperharmonic
+
+/--
+Let $D$ be a finite set of lattice vertices and let
+$\sigma:\mathbb Z[i]\to\mathbb Z$ be an ambient lattice function.  An
+\emph{acyclic indegree orientation with data $\sigma$} chooses exactly one
+direction on every four-neighbor edge of the induced graph on $D$, chooses
+no other directed edges, and has indegree $\sigma(x)$ at each $x\in D$.
+Thus only the restriction of the ambient function $\sigma$ to $D$ supplies
+the prescribed indegrees.  A natural-valued rank strictly increasing along
+every directed edge is included as an explicit certificate of acyclicity.
+-/
+structure AcyclicIndegreeOrientation (D : Finset GaussianInt)
+    (σ : GaussianInt → ℤ) where
+-- BODY
+  /-- The chosen direction of each edge of the finite lattice graph. -/
+  edge : GaussianInt → GaussianInt → Prop
+  /-- Decidable membership in the chosen directed edge relation. -/
+  edgeDecidable : ∀ x y, Decidable (edge x y)
+  /-- A natural rank that increases strictly along each directed edge. -/
+  rank : GaussianInt → ℕ
+  supported : ∀ x y, edge x y →
+    x ∈ D ∧ y ∈ D ∧ FourNeighborAdjacent x y
+  oriented : ∀ x ∈ D, ∀ y ∈ D, FourNeighborAdjacent x y →
+    (edge x y ∧ ¬ edge y x) ∨ (edge y x ∧ ¬ edge x y)
+  increasing : ∀ x y, edge x y → rank x < rank y
+  indegree : ∀ x ∈ D,
+    ((D.filter fun y => @decide (edge y x) (edgeDecidable y x)).card : ℤ) = σ x
+
+end ApollonianSuperharmonic
+
+end

LeanPool/ApollonianSuperharmonic/AdjacentCellInterior.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+module
+
+public import LeanPool.ApollonianSuperharmonic.OpenLatticeEdge
+public import LeanPool.ApollonianSuperharmonic.TileRealization
+public import Mathlib.Topology.Algebra.Ring.Real
+public import Mathlib.Topology.Constructions.SumProd
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+
+/-!
+# Interiors of adjacent lattice cells
+
+Shared open-rectangle arguments adapted from Wesley Pegden's Apache-2.0
+Trellis formalization of Levine–Pegden–Smart. No disk or circle hypotheses are needed.
+-/
+
+@[expose] public section
+
+namespace ApollonianSuperharmonic.AdjacentCellInterior
+
+/-- The common horizontal edge of two cells lies inside their tile realization. -/
+theorem horizontal (U : ProtoTile) (z : GaussianInt)
+    (hu : z ∈ U.cells) (hl : z - ⟨0, 1⟩ ∈ U.cells) :
+    OpenLatticeEdge z (z + 1) ⊆ interior (TileRealization U) := by
+  classical
+  as_aux_lemma =>
+  let R := Set.Ioo (z.re : ℝ) ((z.re : ℝ) + 1) ×ˢ
+    Set.Ioo ((z.im : ℝ) - 1) ((z.im : ℝ) + 1)
+  have hopen : IsOpen R := isOpen_Ioo.prod isOpen_Ioo
+  have hsub : R ⊆ TileRealization U := by
+    intro p hp
+    rcases hp with ⟨⟨hxl, hxu⟩, ⟨hyl, hyu⟩⟩
+    by_cases hside : p.2 ≤ (z.im : ℝ)
+    · apply Set.mem_iUnion.mpr
+      refine ⟨z - ⟨0, 1⟩, Set.mem_iUnion.mpr ⟨hl, ?_⟩⟩
+      simp only [ClosedSquareRealization, Set.mem_Icc, Prod.le_def]
+      norm_num
+      rw [GaussianInt.toComplex_def₂]
+      change ((z.re : ℝ) ≤ p.1 ∧ (z.im : ℝ) ≤ p.2 + 1) ∧
+        (p.1 ≤ (z.re : ℝ) + 1 ∧ p.2 ≤ (z.im : ℝ))
+      constructor <;> constructor <;> linarith
+    · apply Set.mem_iUnion.mpr
+      refine ⟨z, Set.mem_iUnion.mpr ⟨hu, ?_⟩⟩
+      simp only [ClosedSquareRealization, Set.mem_Icc, Prod.le_def]
+      constructor <;> constructor <;> linarith
+  intro p hp
+  apply hopen.subset_interior_iff.mpr hsub
+  rcases hp with ⟨t, ht0, ht1, rfl⟩
+  norm_num [R, GaussianRealPoint, Prod.smul_fst, Prod.smul_snd, smul_eq_mul]
+  constructor <;> constructor <;> nlinarith
+
+/-- The common vertical edge of two cells lies inside their tile realization. -/
+theorem vertical (U : ProtoTile) (z : GaussianInt)
+    (hr : z ∈ U.cells) (hl : z - 1 ∈ U.cells) :
+    OpenLatticeEdge z (z + ⟨0, 1⟩) ⊆ interior (TileRealization U) := by
+  classical
+  as_aux_lemma =>
+  let R := Set.Ioo ((z.re : ℝ) - 1) ((z.re : ℝ) + 1) ×ˢ
+    Set.Ioo (z.im : ℝ) ((z.im : ℝ) + 1)
+  have hopen : IsOpen R := isOpen_Ioo.prod isOpen_Ioo
+  have hsub : R ⊆ TileRealization U := by
+    intro p hp
+    rcases hp with ⟨⟨hxl, hxu⟩, ⟨hyl, hyu⟩⟩
+    by_cases hside : p.1 ≤ (z.re : ℝ)
+    · apply Set.mem_iUnion.mpr
+      refine ⟨z - 1, Set.mem_iUnion.mpr ⟨hl, ?_⟩⟩
+      simp only [ClosedSquareRealization, Set.mem_Icc, Prod.le_def]
+      norm_num
+      rw [GaussianInt.toComplex_def₂]
+      change ((z.re : ℝ) ≤ p.1 + 1 ∧ (z.im : ℝ) ≤ p.2) ∧
+        (p.1 ≤ (z.re : ℝ) ∧ p.2 ≤ (z.im : ℝ) + 1)
+      constructor <;> constructor <;> linarith
+    · apply Set.mem_iUnion.mpr
+      refine ⟨z, Set.mem_iUnion.mpr ⟨hr, ?_⟩⟩
+      simp only [ClosedSquareRealization, Set.mem_Icc, Prod.le_def]
+      constructor <;> constructor <;> linarith
+  intro p hp
+  apply hopen.subset_interior_iff.mpr hsub
+  rcases hp with ⟨t, ht0, ht1, rfl⟩
+  norm_num [R, GaussianRealPoint, Prod.smul_fst, Prod.smul_snd, smul_eq_mul]
+  constructor <;> constructor <;> nlinarith
+
+end ApollonianSuperharmonic.AdjacentCellInterior
+
+end

LeanPool/ApollonianSuperharmonic/AffineLineMapProperties.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+module
+
+public import Mathlib.Basic.Real.Basic
+public import Mathlib.Init
+public import Mathlib.LinearAlgebra.AffineSpace.AffineMap
+public import Mathlib.Tactic.Module
+
+
+/-!
+# AffineLineMapProperties
+
+Shared facts adapted from Wesley Pegden's Apache-2.0 Trellis formalization of
+Levine–Pegden–Smart, replacing repeated implementations at their common dependency level.
+-/
+
+@[expose] public section
+
+namespace ApollonianSuperharmonic
+namespace AffineLineMapProperties
+
+/-- Shared coordinates identity for AffineLineMapProperties. -/
+theorem coordinates :
+    (by
+      classical
+      exact
+        ∀ x y : Real × Real, ∀ t : Real, AffineMap.lineMap x y t = x + t • (y - x) ) := by
+  classical
+  intro x y t
+  rw [AffineMap.lineMap_apply_module]
+  module
+
+end AffineLineMapProperties
+end ApollonianSuperharmonic
+
+end