Audit OEIS A263135 focused Lean target

FormalConjectures/OEIS/263135.lean

@@ -0,0 +1,197 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Maximum contacts on the honeycomb lattice
+
+OEIS A263135 is the maximum number of contacts among `m` vertices of the
+infinite honeycomb graph.  The conjectured even-index closed form is
+
+`A263135 (2 * n) = 3 * n - ceil (sqrt (3 * n))`.
+
+This file gives a concrete coordinate model of the infinite honeycomb graph
+and states that exact extremal theorem.  It also contains the fully proved
+integer ceiling arithmetic that turns the closed form into Peter Kagey's OEIS
+identity with A047932 and A216256.
+
+*References:*
+- [A263135](https://oeis.org/A263135)
+- [A047932](https://oeis.org/A047932)
+- [A216256](https://oeis.org/A216256)
+- Berit Grußien, ["Isoperimetric Inequalities on Hexagonal Grids"](https://arxiv.org/abs/1201.0697)
+-/
+
+namespace OeisA263135
+
+/-- The three edge directions incident to a vertex of the honeycomb graph. -/
+inductive Direction
+  | same
+  | horizontal
+  | diagonal
+  deriving DecidableEq, Fintype
+
+/-- A vertex `A i j` (`side = false`) or `B i j` (`side = true`). -/
+structure Vertex where
+  i : ℤ
+  j : ℤ
+  side : Bool
+  deriving DecidableEq
+
+/-- The neighbor of `v` in direction `d`.
+
+The coordinate convention is
+
+* `A i j ~ B i j`,
+* `A i j ~ B (i - 1) j`,
+* `A i j ~ B i (j - 1)`.
+-/
+def neighbor : Vertex → Direction → Vertex
+  | ⟨i, j, false⟩, .same => ⟨i, j, true⟩
+  | ⟨i, j, false⟩, .horizontal => ⟨i - 1, j, true⟩
+  | ⟨i, j, false⟩, .diagonal => ⟨i, j - 1, true⟩
+  | ⟨i, j, true⟩, .same => ⟨i, j, false⟩
+  | ⟨i, j, true⟩, .horizontal => ⟨i + 1, j, false⟩
+  | ⟨i, j, true⟩, .diagonal => ⟨i, j + 1, false⟩
+
+@[simp]
+theorem neighbor_neighbor (v : Vertex) (d : Direction) :
+    neighbor (neighbor v d) d = v := by
+  rcases v with ⟨i, j, side⟩
+  cases side <;> cases d <;> simp [neighbor]
+
+@[simp]
+theorem neighbor_ne (v : Vertex) (d : Direction) : neighbor v d ≠ v := by
+  rcases v with ⟨i, j, side⟩
+  cases side <;> cases d <;> simp [neighbor]
+
+/-- The number of honeycomb edges with both endpoints in `S`.
+
+Every honeycomb edge has exactly one endpoint on the `A` side, so summing the
+three neighbor tests only over `A` vertices counts every contact exactly once.
+-/
+def contacts (S : Finset Vertex) : ℕ :=
+  ∑ v in S, if v.side = true then 0 else
+    ∑ d : Direction, if neighbor v d ∈ S then 1 else 0
+
+/-- `k` is the maximum contact count among all `N`-vertex honeycomb subsets. -/
+def IsMaximumContact (N k : ℕ) : Prop :=
+  (∃ S : Finset Vertex, S.card = N ∧ contacts S = k) ∧
+    ∀ S : Finset Vertex, S.card = N → contacts S ≤ k
+
+/-- Exact natural-number characterization of `r = ceil (sqrt x)` for positive `x`. -/
+def IsNatCeilSqrt (x r : ℕ) : Prop :=
+  (r - 1) ^ 2 < x ∧ x ≤ r ^ 2
+
+/-- Integer interval characterizing `ceil (sqrt x)` for positive `x`. -/
+def IsCeilSqrt (x r : ℤ) : Prop :=
+  0 ≤ r ∧ (r - 1) ^ 2 < x ∧ x ≤ r ^ 2
+
+/-- Integer interval characterizing A216256 at positive index `n`. -/
+def IsA216256Index (n k : ℤ) : Prop :=
+  0 ≤ k ∧ k ^ 2 - k + 1 < 3 * n ∧ 3 * n ≤ k ^ 2 + k + 1
+
+private lemma isCeilSqrt_unique {x a b : ℤ} (hx : 0 < x)
+    (ha : IsCeilSqrt x a) (hb : IsCeilSqrt x b) : a = b := by
+  rcases ha with ⟨ha0, haLower, haUpper⟩
+  rcases hb with ⟨hb0, hbLower, hbUpper⟩
+  by_contra hne
+  rcases lt_or_gt_of_ne hne with hab | hba
+  · have hb1 : 1 ≤ b := by
+      by_contra h
+      have hbzero : b = 0 := by omega
+      subst b
+      norm_num at hbUpper
+      linarith
+    have h1 : 0 ≤ b - 1 - a := by omega
+    have h2 : 0 ≤ b - 1 + a := by omega
+    have hsq : a ^ 2 ≤ (b - 1) ^ 2 := by
+      nlinarith [mul_nonneg h1 h2]
+    nlinarith
+  · have ha1 : 1 ≤ a := by
+      by_contra h
+      have hazero : a = 0 := by omega
+      subst a
+      norm_num at haUpper
+      linarith
+    have h1 : 0 ≤ a - 1 - b := by omega
+    have h2 : 0 ≤ a - 1 + b := by omega
+    have hsq : b ^ 2 ≤ (a - 1) ^ 2 := by
+      nlinarith [mul_nonneg h1 h2]
+    nlinarith
+
+/-- The exact ceiling subtraction needed after the honeycomb closed form is known. -/
+@[category API, AMS 11]
+theorem ceiling_difference
+    (n k r s : ℤ)
+    (hn : 1 ≤ n)
+    (hk : IsA216256Index n k)
+    (hr : IsCeilSqrt (3 * n) r)
+    (hs : IsCeilSqrt (12 * n - 3) s) :
+    s - r = k := by
+  rcases hk with ⟨hk0, hkLower, hkUpper⟩
+  rcases hr with ⟨hr0, hrLower, hrUpper⟩
+  have hk1 : 1 ≤ k := by
+    by_contra h
+    have hkzero : k = 0 := by omega
+    subst k
+    norm_num at hkUpper
+    nlinarith
+  have hk_le_r : k ≤ r := by
+    by_contra h
+    have hrk : r ≤ k - 1 := by omega
+    have h1 : 0 ≤ k - 1 - r := by omega
+    have h2 : 0 ≤ k - 1 + r := by omega
+    have hsq : r ^ 2 ≤ (k - 1) ^ 2 := by
+      nlinarith [mul_nonneg h1 h2]
+    nlinarith
+  have hr_le : r ≤ k + 1 := by
+    by_contra h
+    have hkr : k + 2 ≤ r := by omega
+    have h1 : 0 ≤ r - 1 - (k + 1) := by omega
+    have h2 : 0 ≤ r - 1 + (k + 1) := by omega
+    have hsq : (k + 1) ^ 2 ≤ (r - 1) ^ 2 := by
+      nlinarith [mul_nonneg h1 h2]
+    nlinarith
+  rcases (show r = k ∨ r = k + 1 by omega) with hrEq | hrEq
+  · subst r
+    have hx : 0 < 12 * n - 3 := by nlinarith
+    have htarget : IsCeilSqrt (12 * n - 3) (2 * k) := by
+      refine ⟨by omega, ?_, ?_⟩ <;> nlinarith
+    have hsEq : s = 2 * k := isCeilSqrt_unique hx hs htarget
+    omega
+  · subst r
+    have hrLower' : k ^ 2 < 3 * n := by simpa using hrLower
+    have hgap : k ^ 2 + 1 ≤ 3 * n := by omega
+    have hx : 0 < 12 * n - 3 := by nlinarith
+    have htarget : IsCeilSqrt (12 * n - 3) (2 * k + 1) := by
+      refine ⟨by omega, ?_, ?_⟩ <;> nlinarith
+    have hsEq : s = 2 * k + 1 := isCeilSqrt_unique hx hs htarget
+    omega
+
+/--
+**OEIS A263135, stronger even-index form.** For every positive `n`, the maximum
+number of contacts among `2 * n` vertices of the infinite honeycomb graph is
+`3 * n - ceil (sqrt (3 * n))`.
+-/
+@[category research open, AMS 05]
+theorem conjecture (n : ℕ) (hn : 0 < n) :
+    ∃ r : ℕ, IsNatCeilSqrt (3 * n) r ∧
+      IsMaximumContact (2 * n) (3 * n - r) := by
+  sorry
+
+end OeisA263135

Scratch/A263135Audit.lean

@@ -0,0 +1,4 @@
+import Scratch.A263135Final
+
+#check OeisA263135.conjecture_solved
+#print axioms OeisA263135.conjecture_solved

Scratch/A263135Boundary.lean

@@ -0,0 +1,40 @@
+import Scratch.A263135Rows
+
+namespace OeisA263135
+
+/-- Row directions preserved by a directed honeycomb edge. -/
+def preservedRows (vd : Vertex × Direction) : Finset RowKind :=
+  Finset.univ.filter fun r => rowCoord r (neighbor vd.1 vd.2) = rowCoord r vd.1
+
+@[simp]
+theorem card_preservedRows (v : Vertex) (d : Direction) :
+    (preservedRows (v, d)).card = 2 := by
+  rcases v with ⟨i, j, side⟩
+  cases side <;> cases d <;>
+    simp [preservedRows, rowCoord, neighbor]
+
+/-- Boundary darts lying along the rows of kind `r`. -/
+def rowBoundaryDarts (r : RowKind) (S : Finset Vertex) : Finset (Vertex × Direction) :=
+  (boundaryDarts S).filter fun vd => r ∈ preservedRows vd
+
+/-- Every boundary dart is counted in exactly two of the three row families. -/
+theorem sum_rowBoundaryDarts_card (S : Finset Vertex) :
+    (∑ r : RowKind, (rowBoundaryDarts r S).card) = 2 * edgeBoundary S := by
+  classical
+  simp_rw [rowBoundaryDarts, Finset.card_eq_sum_ones, Finset.sum_filter]
+  rw [Finset.sum_comm]
+  simp only [edgeBoundary]
+  calc
+    (∑ vd ∈ boundaryDarts S, ∑ r : RowKind, if r ∈ preservedRows vd then 1 else 0) =
+        ∑ vd ∈ boundaryDarts S, (preservedRows vd).card := by
+          apply Finset.sum_congr rfl
+          intro vd hv
+          simp [Finset.card_eq_sum_ones]
+    _ = ∑ _vd ∈ boundaryDarts S, 2 := by
+          apply Finset.sum_congr rfl
+          intro vd hv
+          rcases vd with ⟨v, d⟩
+          simp
+    _ = 2 * (boundaryDarts S).card := by simp [mul_comm]
+
+end OeisA263135

Scratch/A263135BoxChains.lean

@@ -0,0 +1,118 @@
+import Scratch.A263135Ranks
+
+namespace OeisA263135
+
+/-- A ranked honeycomb vertex, forgetting the actual integer row labels. -/
+structure RankPoint where
+  first : ℕ
+  second : ℕ
+  side : Bool
+  deriving DecidableEq
+
+/-- Embedding of the vertical leg of a rectangle chain. -/
+def verticalEmbedding (t : ℕ) (side : Bool) : ℕ ↪ RankPoint where
+  toFun j := ⟨t, j, side⟩
+  inj' := by
+    intro x y h
+    exact congrArg RankPoint.second h
+
+/-- Embedding of the horizontal leg of a rectangle chain. -/
+def horizontalEmbedding (t b : ℕ) (side : Bool) : ℕ ↪ RankPoint where
+  toFun h := ⟨t + 1 + h, b - 1 - t, side⟩
+  inj' := by
+    intro x y h
+    have := congrArg RankPoint.first h
+    omega
+
+/-- Vertical part of the `t`-th symmetric chain in an `a × b` rectangle. -/
+def verticalChain (b t : ℕ) (side : Bool) : Finset RankPoint :=
+  (Finset.range (b - t)).map (verticalEmbedding t side)
+
+/-- Horizontal part after the corner of the `t`-th rectangle chain. -/
+def horizontalChain (a b t : ℕ) (side : Bool) : Finset RankPoint :=
+  (Finset.range (a - 1 - t)).map (horizontalEmbedding t b side)
+
+/-- The full `t`-th symmetric chain of rectangle cells, on one fixed honeycomb side. -/
+def baseBoxChain (a b t : ℕ) (side : Bool) : Finset RankPoint :=
+  verticalChain b t side ∪ horizontalChain a b t side
+
+private theorem vertical_horizontal_disjoint (a b t : ℕ) (side : Bool) :
+    Disjoint (verticalChain b t side) (horizontalChain a b t side) := by
+  rw [Finset.disjoint_left]
+  intro p hpv hph
+  rcases Finset.mem_map.mp hpv with ⟨j, hj, hjp⟩
+  rcases Finset.mem_map.mp hph with ⟨h, hh, hhp⟩
+  have heq : (verticalEmbedding t side j).first =
+      (horizontalEmbedding t b side h).first := by
+    rw [hjp, hhp]
+  simp [verticalEmbedding, horizontalEmbedding] at heq
+  omega
+
+/-- Cardinality of a base rectangle chain. -/
+theorem card_baseBoxChain (a b t : ℕ) (side : Bool)
+    (ht : t < a) (hab : a ≤ b) :
+    (baseBoxChain a b t side).card = a + b - 1 - 2 * t := by
+  rw [baseBoxChain, Finset.card_union_of_disjoint
+    (vertical_horizontal_disjoint a b t side)]
+  simp [verticalChain, horizontalChain]
+  omega
+
+/-- Last rectangle cell of the `t`-th chain. -/
+def lastRankPoint (a b t : ℕ) (side : Bool) : RankPoint :=
+  ⟨a - 1, b - 1 - t, side⟩
+
+private theorem lastRankPoint_mem_baseBoxChain (a b t : ℕ) (side : Bool)
+    (ht : t < a) (hab : a ≤ b) :
+    lastRankPoint a b t side ∈ baseBoxChain a b t side := by
+  by_cases hlast : t = a - 1
+  · apply Finset.mem_union_left
+    apply Finset.mem_map.mpr
+    refine ⟨b - 1 - t, ?_, ?_⟩
+    · simp only [Finset.mem_range]
+      omega
+    · apply RankPoint.ext <;> simp [verticalEmbedding, lastRankPoint, hlast]
+  · apply Finset.mem_union_right
+    apply Finset.mem_map.mpr
+    refine ⟨a - 2 - t, ?_, ?_⟩
+    · simp only [Finset.mem_range]
+      omega
+    · apply RankPoint.ext <;> simp [horizontalEmbedding, lastRankPoint]
+      omega
+
+/-- Long product chain: every `A` cell of a base chain followed by its final `B` cell. -/
+def longBoxChain (a b t : ℕ) : Finset RankPoint :=
+  baseBoxChain a b t false ∪ {lastRankPoint a b t true}
+
+/-- Short product chain: every `B` cell except the final cell of the base chain. -/
+def shortBoxChain (a b t : ℕ) : Finset RankPoint :=
+  (baseBoxChain a b t true).erase (lastRankPoint a b t true)
+
+private theorem base_false_disjoint_last_true (a b t : ℕ) :
+    Disjoint (baseBoxChain a b t false) {lastRankPoint a b t true} := by
+  rw [Finset.disjoint_singleton_right]
+  intro h
+  rcases Finset.mem_union.mp h with h | h
+  · rcases Finset.mem_map.mp h with ⟨j, hj, heq⟩
+    have := congrArg RankPoint.side heq
+    simp [verticalEmbedding, lastRankPoint] at this
+  · rcases Finset.mem_map.mp h with ⟨k, hk, heq⟩
+    have := congrArg RankPoint.side heq
+    simp [horizontalEmbedding, lastRankPoint] at this
+
+/-- Length of the long product chain. -/
+theorem card_longBoxChain (a b t : ℕ) (ht : t < a) (hab : a ≤ b) :
+    (longBoxChain a b t).card = a + b - 2 * t := by
+  rw [longBoxChain, Finset.card_union_of_disjoint
+    (base_false_disjoint_last_true a b t), card_baseBoxChain _ _ _ _ ht hab]
+  simp
+  omega
+
+/-- Length of the short product chain. -/
+theorem card_shortBoxChain (a b t : ℕ) (ht : t < a) (hab : a ≤ b) :
+    (shortBoxChain a b t).card = a + b - 2 - 2 * t := by
+  rw [shortBoxChain, Finset.card_erase_of_mem
+    (lastRankPoint_mem_baseBoxChain a b t true ht hab),
+    card_baseBoxChain _ _ _ _ ht hab]
+  omega
+
+end OeisA263135