diff --git a/FormalConjectures/OEIS/263135.lean b/FormalConjectures/OEIS/263135.lean
new file mode 100644
index 0000000000..4be92b3c78
--- /dev/null
+++ b/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
diff --git a/Scratch/A263135Audit.lean b/Scratch/A263135Audit.lean
new file mode 100644
index 0000000000..bd3cf8613e
--- /dev/null
+++ b/Scratch/A263135Audit.lean
@@ -0,0 +1,4 @@
+import Scratch.A263135Final
+
+#check OeisA263135.conjecture_solved
+#print axioms OeisA263135.conjecture_solved
diff --git a/Scratch/A263135Boundary.lean b/Scratch/A263135Boundary.lean
new file mode 100644
index 0000000000..56adbf9131
--- /dev/null
+++ b/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
diff --git a/Scratch/A263135BoxChains.lean b/Scratch/A263135BoxChains.lean
new file mode 100644
index 0000000000..af9b75f123
--- /dev/null
+++ b/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
diff --git a/Scratch/A263135CapArithmetic.lean b/Scratch/A263135CapArithmetic.lean
new file mode 100644
index 0000000000..07a00cbf04
--- /dev/null
+++ b/Scratch/A263135CapArithmetic.lean
@@ -0,0 +1,95 @@
+import Scratch.A263135ChainCount
+
+namespace OeisA263135
+
+private theorem sum_sub_two_mul_eq_staircase (q a : ℕ) (hqa : q ≤ a) :
+    (∑ t ∈ Finset.range a, q - 2 * t) = staircase q := by
+  unfold staircase
+  nth_rewrite 1 [← Nat.add_sub_of_le hqa]
+  rw [Finset.sum_range_add]
+  have hzero : (∑ t ∈ Finset.range (a - q), q - 2 * (q + t)) = 0 := by
+    apply Finset.sum_eq_zero
+    intro t ht
+    omega
+  rw [hzero, add_zero]
+
+private theorem min_long_add_deficit (a b c t : ℕ) :
+    min c (a + b - 2 * t) + (a + b - c - 2 * t) = a + b - 2 * t := by
+  by_cases h : c ≤ a + b - 2 * t
+  · rw [min_eq_left h]
+    omega
+  · rw [min_eq_right (Nat.le_of_not_ge h)]
+    omega
+
+private theorem min_short_add_deficit (a b c t : ℕ) :
+    min c (a + b - 2 - 2 * t) + (a + b - c - 2 - 2 * t) =
+      a + b - 2 - 2 * t := by
+  by_cases h : c ≤ a + b - 2 - 2 * t
+  · rw [min_eq_left h]
+    omega
+  · rw [min_eq_right (Nat.le_of_not_ge h)]
+    omega
+
+private theorem sum_chain_lengths (a b : ℕ) (hab : a ≤ b) :
+    (∑ t ∈ Finset.range a,
+      ((a + b - 2 * t) + (a + b - 2 - 2 * t))) = 2 * a * b := by
+  have hterm : ∀ t ∈ Finset.range a,
+      ((a + b - 2 * t) + (a + b - 2 - 2 * t)) + 4 * t =
+        2 * (a + b - 1) := by
+    intro t ht
+    have hta := Finset.mem_range.mp ht
+    omega
+  have hsum := Finset.sum_congr rfl hterm
+  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range,
+    Nat.nsmul_eq_mul] at hsum
+  have hfour : (∑ t ∈ Finset.range a, 4 * t) =
+      4 * ∑ t ∈ Finset.range a, t := by
+    rw [Finset.mul_sum]
+  rw [hfour] at hsum
+  have hgauss := Finset.sum_range_id_mul_two a
+  nlinarith
+
+/-- The total unused capacity of the product chains is the staircase deficiency. -/
+theorem chainCapSum_add_deficiency (a b c : ℕ)
+    (hab : a ≤ b) (hbc : b ≤ c) :
+    chainCapSum a b c + staircaseDeficiency (a + b - c) = 2 * a * b := by
+  let q := a + b - c
+  have hqa : q ≤ a := by
+    dsimp [q]
+    omega
+  have hq2a : q - 2 ≤ a := by omega
+  have hdef1 := sum_sub_two_mul_eq_staircase q a hqa
+  have hdef2 := sum_sub_two_mul_eq_staircase (q - 2) a hq2a
+  have hterm : ∀ t ∈ Finset.range a,
+      (min c (a + b - 2 * t) + min c (a + b - 2 - 2 * t)) +
+          ((q - 2 * t) + (q - 2 - 2 * t)) =
+        (a + b - 2 * t) + (a + b - 2 - 2 * t) := by
+    intro t ht
+    dsimp [q]
+    rw [← min_long_add_deficit a b c t, ← min_short_add_deficit a b c t]
+    omega
+  have hsum := Finset.sum_congr rfl hterm
+  simp only [Finset.sum_add_distrib] at hsum
+  unfold chainCapSum staircaseDeficiency
+  rw [← hdef1, ← hdef2]
+  simp only [Finset.sum_add_distrib]
+  rw [sum_chain_lengths a b hab] at hsum
+  omega
+
+/-- Sorted row counts imply the required quadratic size bound. -/
+theorem six_mul_card_le_row_sum_sq_of_sorted (S : Finset Vertex)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card)
+    (hbc : (occupiedRows .second S).card ≤ (occupiedRows .diagonal S).card) :
+    6 * S.card ≤
+      ((occupiedRows .first S).card + (occupiedRows .second S).card +
+        (occupiedRows .diagonal S).card) ^ 2 := by
+  let a := (occupiedRows .first S).card
+  let b := (occupiedRows .second S).card
+  let c := (occupiedRows .diagonal S).card
+  have hcard := card_le_chainCapSum S hab
+  have hcap := chainCapSum_add_deficiency a b c hab hbc
+  have hm : S.card + staircaseDeficiency (a + b - c) ≤ 2 * a * b := by
+    omega
+  exact perimeter_square_of_chain_deficiency a b c S.card hab hbc hm
+
+end OeisA263135
diff --git a/Scratch/A263135ChainCount.lean b/Scratch/A263135ChainCount.lean
new file mode 100644
index 0000000000..23d2a320cf
--- /dev/null
+++ b/Scratch/A263135ChainCount.lean
@@ -0,0 +1,140 @@
+import Scratch.A263135ChainOrder
+
+namespace OeisA263135
+
+/-- Finite key set indexing all long and short product chains. -/
+def chainKeys (S : Finset Vertex) : Finset (ℕ × Bool) :=
+  Finset.range (occupiedRows .first S).card ×ˢ Finset.univ
+
+/-- Chain key of a selected honeycomb vertex. -/
+noncomputable def vertexChainKey (S : Finset Vertex) (v : ↥S) : ℕ × Bool :=
+  (vertexChainIndex S v, vertexSubchain S v)
+
+/-- Vertices of `S` assigned to one product chain. -/
+noncomputable def chainFiber (S : Finset Vertex) (k : ℕ × Bool) : Finset ↥S :=
+  S.attach.filter fun v => vertexChainKey S v = k
+
+/-- Sum of the long- and short-chain capacity bounds. -/
+def chainCapSum (a b c : ℕ) : ℕ :=
+  ∑ t ∈ Finset.range a,
+    (min c (a + b - 2 * t) + min c (a + b - 2 - 2 * t))
+
+private theorem vertexChainKey_mem (S : Finset Vertex) (v : ↥S) :
+    vertexChainKey S v ∈ chainKeys S := by
+  simp [vertexChainKey, chainKeys, vertexChainIndex_lt_firstRows]
+
+/-- The selected vertices partition into product-chain fibers. -/
+theorem card_eq_sum_chainFiber (S : Finset Vertex) :
+    S.card = ∑ k ∈ chainKeys S, (chainFiber S k).card := by
+  rw [← Finset.card_attach]
+  exact Finset.card_eq_sum_card_fiberwise fun v _ => vertexChainKey_mem S v
+
+private theorem chainFiber_key {S : Finset Vertex} {k : ℕ × Bool} {v : ↥S}
+    (hv : v ∈ chainFiber S k) : vertexChainKey S v = k :=
+  (Finset.mem_filter.mp hv).2
+
+private theorem chainFiber_rankPoint_mem
+    {S : Finset Vertex} {k : ℕ × Bool} {v : ↥S}
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card)
+    (hv : v ∈ chainFiber S k) :
+    if k.2 then
+      vertexRankPoint S v ∈
+        shortBoxChain (occupiedRows .first S).card (occupiedRows .second S).card k.1
+    else
+      vertexRankPoint S v ∈
+        longBoxChain (occupiedRows .first S).card (occupiedRows .second S).card k.1 := by
+  have hchosen := vertexRankPoint_mem_chosenChain S v hab
+  have hkey := chainFiber_key hv
+  have ht := congrArg Prod.fst hkey
+  have hs := congrArg Prod.snd hkey
+  simpa [vertexChainKey, ht, hs] using hchosen
+
+private theorem chainFiber_card_le_boxChain
+    (S : Finset Vertex) (k : ℕ × Bool)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card) :
+    (chainFiber S k).card ≤
+      if k.2 then
+        (shortBoxChain (occupiedRows .first S).card (occupiedRows .second S).card k.1).card
+      else
+        (longBoxChain (occupiedRows .first S).card (occupiedRows .second S).card k.1).card := by
+  classical
+  cases hk : k.2
+  · apply Finset.card_le_card_of_injOn (vertexRankPoint S)
+    · intro v hv
+      simpa [hk] using chainFiber_rankPoint_mem hab hv
+    · intro v hv w hw h
+      exact vertexRankPoint_injective S h
+  · apply Finset.card_le_card_of_injOn (vertexRankPoint S)
+    · intro v hv
+      simpa [hk] using chainFiber_rankPoint_mem hab hv
+    · intro v hv w hw h
+      exact vertexRankPoint_injective S h
+
+private theorem chainFiber_card_le_diagonalRows
+    (S : Finset Vertex) (k : ℕ × Bool)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card) :
+    (chainFiber S k).card ≤ (occupiedRows .diagonal S).card := by
+  classical
+  have hinj : Set.InjOn (rowLabel .diagonal S) (chainFiber S k) := by
+    intro v hv w hw hlabel
+    have hkeyv := chainFiber_key hv
+    have hkeyw := chainFiber_key hw
+    have ht : vertexChainIndex S v = vertexChainIndex S w := by
+      have hvf := congrArg Prod.fst hkeyv
+      have hwf := congrArg Prod.fst hkeyw
+      exact hvf.trans hwf.symm
+    have hdiag : rowCoord .diagonal v = rowCoord .diagonal w := by
+      exact congrArg Subtype.val hlabel
+    have hvchain := chainFiber_rankPoint_mem hab hv
+    have hwchain := chainFiber_rankPoint_mem hab hw
+    cases hk : k.2
+    · exact diagonal_injective_on_longChain S v w hab ht
+        (by simpa [hk] using hvchain) (by simpa [hk] using hwchain) hdiag
+    · exact diagonal_injective_on_shortChain S v w ht
+        (by simpa [hk] using hvchain) (by simpa [hk] using hwchain) hdiag
+  have hcard := Finset.card_le_card_of_injOn (rowLabel .diagonal S)
+    (t := (Finset.univ : Finset ↥(occupiedRows .diagonal S)))
+    (fun _ _ => Finset.mem_univ _) hinj
+  simpa using hcard
+
+private theorem chainFiber_card_le_capacity
+    (S : Finset Vertex) (k : ℕ × Bool)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card) :
+    (chainFiber S k).card ≤
+      min (occupiedRows .diagonal S).card
+        (if k.2 then
+          (shortBoxChain (occupiedRows .first S).card (occupiedRows .second S).card k.1).card
+        else
+          (longBoxChain (occupiedRows .first S).card (occupiedRows .second S).card k.1).card) := by
+  exact le_min (chainFiber_card_le_diagonalRows S k hab)
+    (chainFiber_card_le_boxChain S k hab)
+
+/-- Cardinality bound obtained by summing capacities of the symmetric chains. -/
+theorem card_le_chainCapSum (S : Finset Vertex)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card) :
+    S.card ≤ chainCapSum (occupiedRows .first S).card
+      (occupiedRows .second S).card (occupiedRows .diagonal S).card := by
+  classical
+  rw [card_eq_sum_chainFiber]
+  calc
+    (∑ k ∈ chainKeys S, (chainFiber S k).card) ≤
+        ∑ k ∈ chainKeys S,
+          min (occupiedRows .diagonal S).card
+            (if k.2 then
+              (shortBoxChain (occupiedRows .first S).card
+                (occupiedRows .second S).card k.1).card
+            else
+              (longBoxChain (occupiedRows .first S).card
+                (occupiedRows .second S).card k.1).card) := by
+          exact Finset.sum_le_sum fun k _ => chainFiber_card_le_capacity S k hab
+    _ = chainCapSum (occupiedRows .first S).card
+        (occupiedRows .second S).card (occupiedRows .diagonal S).card := by
+      unfold chainKeys chainCapSum
+      rw [Finset.sum_product]
+      apply Finset.sum_congr rfl
+      intro t ht
+      have hta : t < (occupiedRows .first S).card := Finset.mem_range.mp ht
+      simp [card_longBoxChain _ _ _ hta hab, card_shortBoxChain _ _ _ hta hab,
+        add_comm]
+
+end OeisA263135
diff --git a/Scratch/A263135ChainMembership.lean b/Scratch/A263135ChainMembership.lean
new file mode 100644
index 0000000000..3b45a3477f
--- /dev/null
+++ b/Scratch/A263135ChainMembership.lean
@@ -0,0 +1,115 @@
+import Scratch.A263135BoxChains
+
+namespace OeisA263135
+
+/-- Pair of the first two occupied-row ranks. -/
+noncomputable def rectangleRankPair (S : Finset Vertex) (v : ↥S) :
+    Fin (occupiedRows .first S).card × Fin (occupiedRows .second S).card :=
+  (rowRank .first S v, rowRank .second S v)
+
+/-- Ranked point corresponding to a honeycomb vertex. -/
+noncomputable def vertexRankPoint (S : Finset Vertex) (v : ↥S) : RankPoint :=
+  ⟨(rowRank .first S v).val, (rowRank .second S v).val, v.val.side⟩
+
+/-- Rectangle-chain index of a honeycomb vertex. -/
+noncomputable def vertexChainIndex (S : Finset Vertex) (v : ↥S) : ℕ :=
+  rectangleChainIndex (rectangleRankPair S v)
+
+/-- Product-chain choice of a honeycomb vertex. -/
+noncomputable def vertexSubchain (S : Finset Vertex) (v : ↥S) : Bool :=
+  boxSubchain (rectangleRankPair S v) v.val.side
+
+/-- A vertex's rectangle-chain index lies in the first-row range. -/
+theorem vertexChainIndex_lt_firstRows (S : Finset Vertex) (v : ↥S) :
+    vertexChainIndex S v < (occupiedRows .first S).card := by
+  unfold vertexChainIndex rectangleChainIndex rectangleRankPair
+  exact lt_of_le_of_lt (Nat.min_le_left _ _) (rowRank .first S v).isLt
+
+private theorem rankPoint_mem_baseBoxChain (S : Finset Vertex) (v : ↥S)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card) :
+    vertexRankPoint S v ∈
+      baseBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+        (vertexChainIndex S v) v.val.side := by
+  let a := (occupiedRows .first S).card
+  let b := (occupiedRows .second S).card
+  let p := rectangleRankPair S v
+  let t := vertexChainIndex S v
+  have hi : p.1.val < a := p.1.isLt
+  have hj : p.2.val < b := p.2.isLt
+  have ht : t = min p.1.val (b - 1 - p.2.val) := rfl
+  by_cases hvertical : p.1.val ≤ b - 1 - p.2.val
+  · apply Finset.mem_union_left
+    apply Finset.mem_map.mpr
+    refine ⟨p.2.val, ?_, ?_⟩
+    · simp only [Finset.mem_range]
+      rw [ht, Nat.min_eq_left hvertical]
+      omega
+    · apply RankPoint.ext <;>
+        simp [vertexRankPoint, rectangleRankPair, verticalEmbedding, t, p, ht,
+          Nat.min_eq_left hvertical]
+  · apply Finset.mem_union_right
+    apply Finset.mem_map.mpr
+    let h := p.1.val - (t + 1)
+    refine ⟨h, ?_, ?_⟩
+    · simp only [Finset.mem_range]
+      rw [ht, Nat.min_eq_right (Nat.le_of_not_ge hvertical)] at *
+      dsimp [h]
+      omega
+    · apply RankPoint.ext <;>
+        simp [vertexRankPoint, rectangleRankPair, horizontalEmbedding, t, p, h, ht,
+          Nat.min_eq_right (Nat.le_of_not_ge hvertical)]
+      omega
+
+private theorem vertexRankPoint_last_iff (S : Finset Vertex) (v : ↥S) :
+    vertexRankPoint S v =
+        lastRankPoint (occupiedRows .first S).card (occupiedRows .second S).card
+          (vertexChainIndex S v) v.val.side ↔
+      isRectangleChainLast (rectangleRankPair S v) := by
+  constructor
+  · intro h
+    constructor
+    · exact congrArg RankPoint.first h
+    · exact congrArg RankPoint.second h
+  · rintro ⟨hi, hj⟩
+    apply RankPoint.ext <;>
+      simp [vertexRankPoint, lastRankPoint, rectangleRankPair, hi, hj]
+
+/-- Every ranked vertex belongs to its chosen long or short product chain. -/
+theorem vertexRankPoint_mem_chosenChain (S : Finset Vertex) (v : ↥S)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card) :
+    if vertexSubchain S v then
+      vertexRankPoint S v ∈
+        shortBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+          (vertexChainIndex S v)
+    else
+      vertexRankPoint S v ∈
+        longBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+          (vertexChainIndex S v) := by
+  have hbase := rankPoint_mem_baseBoxChain S v hab
+  unfold vertexSubchain boxSubchain
+  by_cases hside : v.val.side = true
+  · simp only [hside, Bool.true_and, Bool.decide_coe]
+    by_cases hlast : isRectangleChainLast (rectangleRankPair S v)
+    · simp [hlast, longBoxChain, vertexRankPoint_last_iff.mpr hlast]
+    · simp [hlast, shortBoxChain, hbase, vertexRankPoint_last_iff, hlast]
+  · have hfalse : v.val.side = false := Bool.eq_false_of_not_eq_true hside
+    simp [hfalse, longBoxChain, hbase]
+
+/-- The ranked-point map is injective. -/
+theorem vertexRankPoint_injective (S : Finset Vertex) :
+    Function.Injective (vertexRankPoint S) := by
+  intro v w h
+  have hfirst : rowRank .first S v = rowRank .first S w := by
+    apply Fin.ext
+    exact congrArg RankPoint.first h
+  have hsecond : rowRank .second S v = rowRank .second S w := by
+    apply Fin.ext
+    exact congrArg RankPoint.second h
+  have hside : v.val.side = w.val.side := congrArg RankPoint.side h
+  apply Subtype.ext
+  apply Vertex.ext
+  · simpa [rowCoord] using (rowRank_eq_iff_rowCoord_eq .first S v w).mp hfirst
+  · simpa [rowCoord] using (rowRank_eq_iff_rowCoord_eq .second S v w).mp hsecond
+  · exact hside
+
+end OeisA263135
diff --git a/Scratch/A263135ChainOrder.lean b/Scratch/A263135ChainOrder.lean
new file mode 100644
index 0000000000..dec88e5c44
--- /dev/null
+++ b/Scratch/A263135ChainOrder.lean
@@ -0,0 +1,193 @@
+import Scratch.A263135ChainMembership
+
+namespace OeisA263135
+
+private theorem baseBoxChain_side {a b t : ℕ} {side : Bool} {p : RankPoint}
+    (hp : p ∈ baseBoxChain a b t side) : p.side = side := by
+  rcases Finset.mem_union.mp hp with hp | hp
+  · rcases Finset.mem_map.mp hp with ⟨j, hj, rfl⟩
+    rfl
+  · rcases Finset.mem_map.mp hp with ⟨h, hh, rfl⟩
+    rfl
+
+/-- Any two points on one base rectangle chain are comparable coordinatewise. -/
+theorem baseBoxChain_comparable {a b t : ℕ} {side : Bool} {p q : RankPoint}
+    (hp : p ∈ baseBoxChain a b t side)
+    (hq : q ∈ baseBoxChain a b t side) :
+    (p.first ≤ q.first ∧ p.second ≤ q.second) ∨
+      (q.first ≤ p.first ∧ q.second ≤ p.second) := by
+  rcases Finset.mem_union.mp hp with hp | hp <;>
+    rcases Finset.mem_union.mp hq with hq | hq
+  · rcases Finset.mem_map.mp hp with ⟨j, hj, rfl⟩
+    rcases Finset.mem_map.mp hq with ⟨k, hk, rfl⟩
+    rcases le_total j k with h | h
+    · exact Or.inl ⟨le_rfl, h⟩
+    · exact Or.inr ⟨le_rfl, h⟩
+  · rcases Finset.mem_map.mp hp with ⟨j, hj, rfl⟩
+    rcases Finset.mem_map.mp hq with ⟨h, hh, rfl⟩
+    left
+    simp only [verticalEmbedding, horizontalEmbedding]
+    constructor <;> omega
+  · rcases Finset.mem_map.mp hp with ⟨h, hh, rfl⟩
+    rcases Finset.mem_map.mp hq with ⟨j, hj, rfl⟩
+    right
+    simp only [verticalEmbedding, horizontalEmbedding]
+    constructor <;> omega
+  · rcases Finset.mem_map.mp hp with ⟨h, hh, rfl⟩
+    rcases Finset.mem_map.mp hq with ⟨k, hk, rfl⟩
+    rcases le_total h k with hle | hle
+    · exact Or.inl ⟨by omega, le_rfl⟩
+    · exact Or.inr ⟨by omega, le_rfl⟩
+
+private theorem baseBoxChain_le_last {a b t : ℕ} {side : Bool} {p : RankPoint}
+    (ht : t < a) (hab : a ≤ b)
+    (hp : p ∈ baseBoxChain a b t side) :
+    p.first ≤ (lastRankPoint a b t side).first ∧
+      p.second ≤ (lastRankPoint a b t side).second := by
+  rcases Finset.mem_union.mp hp with hp | hp
+  · rcases Finset.mem_map.mp hp with ⟨j, hj, rfl⟩
+    simp only [verticalEmbedding, lastRankPoint]
+    constructor <;> omega
+  · rcases Finset.mem_map.mp hp with ⟨h, hh, rfl⟩
+    simp only [horizontalEmbedding, lastRankPoint]
+    constructor <;> omega
+
+private theorem longBoxChain_true_eq_last {a b t : ℕ} {p : RankPoint}
+    (hp : p ∈ longBoxChain a b t) (hside : p.side = true) :
+    p = lastRankPoint a b t true := by
+  rcases Finset.mem_union.mp hp with hp | hp
+  · have := baseBoxChain_side hp
+    simp [hside] at this
+  · simpa using Finset.mem_singleton.mp hp
+
+private theorem shortBoxChain_side_true {a b t : ℕ} {p : RankPoint}
+    (hp : p ∈ shortBoxChain a b t) : p.side = true := by
+  exact baseBoxChain_side (Finset.mem_of_mem_erase hp)
+
+private theorem vertex_eq_of_rankPoint_comparable_same_side
+    (S : Finset Vertex) (v w : ↥S)
+    (hside : v.val.side = w.val.side)
+    (hdiag : rowCoord .diagonal v = rowCoord .diagonal w)
+    (hcomp :
+      ((vertexRankPoint S v).first ≤ (vertexRankPoint S w).first ∧
+        (vertexRankPoint S v).second ≤ (vertexRankPoint S w).second) ∨
+      ((vertexRankPoint S w).first ≤ (vertexRankPoint S v).first ∧
+        (vertexRankPoint S w).second ≤ (vertexRankPoint S v).second)) :
+    v = w := by
+  have finish
+      (hfirst : (vertexRankPoint S v).first ≤ (vertexRankPoint S w).first)
+      (hsecond : (vertexRankPoint S v).second ≤ (vertexRankPoint S w).second) : v = w := by
+    have hi := rowCoord_le_of_rowRank_le .first S v w hfirst
+    have hj := rowCoord_le_of_rowRank_le .second S v w hsecond
+    have hieq : rowCoord .first v = rowCoord .first w := by
+      rcases v with ⟨⟨iv, jv, sv⟩, hv⟩
+      rcases w with ⟨⟨iw, jw, sw⟩, hw⟩
+      simp [rowCoord] at hi hj hdiag hside ⊢
+      omega
+    have hjeq : rowCoord .second v = rowCoord .second w := by
+      rcases v with ⟨⟨iv, jv, sv⟩, hv⟩
+      rcases w with ⟨⟨iw, jw, sw⟩, hw⟩
+      simp [rowCoord] at hi hj hdiag hside ⊢
+      omega
+    apply Subtype.ext
+    apply Vertex.ext
+    · simpa [rowCoord] using hieq
+    · simpa [rowCoord] using hjeq
+    · exact hside
+  rcases hcomp with h | h
+  · exact finish h.1 h.2
+  · exact (finish (v := w) (w := v) hside.symm hdiag.symm h.1 h.2).symm
+
+/-- Third-direction row labels are injective on each long product chain. -/
+theorem diagonal_injective_on_longChain
+    (S : Finset Vertex) (v w : ↥S)
+    (hab : (occupiedRows .first S).card ≤ (occupiedRows .second S).card)
+    (ht : vertexChainIndex S v = vertexChainIndex S w)
+    (hv : vertexRankPoint S v ∈
+      longBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+        (vertexChainIndex S v))
+    (hw : vertexRankPoint S w ∈
+      longBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+        (vertexChainIndex S w))
+    (hdiag : rowCoord .diagonal v = rowCoord .diagonal w) :
+    v = w := by
+  by_cases hsv : v.val.side = true <;> by_cases hsw : w.val.side = true
+  · have hvlast := longBoxChain_true_eq_last hv hsv
+    have hwlast := longBoxChain_true_eq_last (ht ▸ hw) hsw
+    apply vertexRankPoint_injective S
+    rw [hvlast, hwlast]
+  · have hvlast := longBoxChain_true_eq_last hv hsv
+    have hwbase : vertexRankPoint S w ∈
+        baseBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+          (vertexChainIndex S v) false := by
+      rcases Finset.mem_union.mp (ht ▸ hw) with h | h
+      · exact h
+      · have hlast := Finset.mem_singleton.mp h
+        have := congrArg RankPoint.side hlast
+        simp [hsw, lastRankPoint] at this
+    have hle := baseBoxChain_le_last
+      (vertexChainIndex_lt_firstRows S v) hab hwbase
+    have hi := rowCoord_le_of_rowRank_le .first S w v hle.1
+    have hj := rowCoord_le_of_rowRank_le .second S w v hle.2
+    rcases v with ⟨⟨iv, jv, sv⟩, hvS⟩
+    rcases w with ⟨⟨iw, jw, sw⟩, hwS⟩
+    simp [rowCoord] at hi hj hdiag hsv hsw
+    omega
+  · have hwlast := longBoxChain_true_eq_last (ht ▸ hw) hsw
+    have hvbase : vertexRankPoint S v ∈
+        baseBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+          (vertexChainIndex S v) false := by
+      rcases Finset.mem_union.mp hv with h | h
+      · exact h
+      · have hlast := Finset.mem_singleton.mp h
+        have := congrArg RankPoint.side hlast
+        simp [hsv, lastRankPoint] at this
+    have hle := baseBoxChain_le_last
+      (vertexChainIndex_lt_firstRows S v) hab hvbase
+    have hi := rowCoord_le_of_rowRank_le .first S v w hle.1
+    have hj := rowCoord_le_of_rowRank_le .second S v w hle.2
+    rcases v with ⟨⟨iv, jv, sv⟩, hvS⟩
+    rcases w with ⟨⟨iw, jw, sw⟩, hwS⟩
+    simp [rowCoord] at hi hj hdiag hsv hsw
+    omega
+  · have hcomp := baseBoxChain_comparable
+      (show vertexRankPoint S v ∈
+        baseBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+          (vertexChainIndex S v) false by
+        rcases Finset.mem_union.mp hv with h | h
+        · exact h
+        · have hlast := Finset.mem_singleton.mp h
+          have := congrArg RankPoint.side hlast
+          simp [hsv, lastRankPoint] at this)
+      (show vertexRankPoint S w ∈
+        baseBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+          (vertexChainIndex S v) false by
+        rcases Finset.mem_union.mp (ht ▸ hw) with h | h
+        · exact h
+        · have hlast := Finset.mem_singleton.mp h
+          have := congrArg RankPoint.side hlast
+          simp [hsw, lastRankPoint] at this)
+    exact vertex_eq_of_rankPoint_comparable_same_side S v w
+      (Bool.eq_false_of_not_eq_true hsv |>.trans
+        (Bool.eq_false_of_not_eq_true hsw).symm) hdiag hcomp
+
+/-- Third-direction row labels are injective on each short product chain. -/
+theorem diagonal_injective_on_shortChain
+    (S : Finset Vertex) (v w : ↥S)
+    (ht : vertexChainIndex S v = vertexChainIndex S w)
+    (hv : vertexRankPoint S v ∈
+      shortBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+        (vertexChainIndex S v))
+    (hw : vertexRankPoint S w ∈
+      shortBoxChain (occupiedRows .first S).card (occupiedRows .second S).card
+        (vertexChainIndex S w))
+    (hdiag : rowCoord .diagonal v = rowCoord .diagonal w) :
+    v = w := by
+  have hcomp := baseBoxChain_comparable
+    (Finset.mem_of_mem_erase hv)
+    (Finset.mem_of_mem_erase (ht ▸ hw))
+  exact vertex_eq_of_rankPoint_comparable_same_side S v w
+    ((shortBoxChain_side_true hv).trans (shortBoxChain_side_true (ht ▸ hw)).symm)
+    hdiag hcomp
+
+end OeisA263135
diff --git a/Scratch/A263135ClippingCard.lean b/Scratch/A263135ClippingCard.lean
new file mode 100644
index 0000000000..58d1731eb0
--- /dev/null
+++ b/Scratch/A263135ClippingCard.lean
@@ -0,0 +1,67 @@
+import Scratch.A263135PatchContacts
+
+namespace OeisA263135
+
+/-- The two vertices of a clipping pair are distinct. -/
+theorem card_clipPair (a b k : ℕ) : (clipPair a b k).card = 2 := by
+  unfold clipPair
+  split_ifs <;> simp
+
+private theorem clipPair_pairwise_disjoint
+    (a b d : ℕ) (hd : d ≤ a + b - 1) :
+    (Finset.range d).toSet.PairwiseDisjoint (clipPair a b) := by
+  intro k hk l hl hkl
+  have hkd : k < d := Finset.mem_range.mp hk
+  have hld : l < d := Finset.mem_range.mp hl
+  rw [Finset.disjoint_left]
+  intro p hpk hpl
+  by_cases hkb : k < b <;> by_cases hlb : l < b <;>
+    simp [clipPair, hkb, hlb] at hpk hpl <;>
+    rcases hpk with (rfl | rfl) <;> rcases hpl with h | h <;>
+    simp at h <;> omega
+
+/-- The first `d` clipping pairs contain exactly `2d` distinct ranked vertices. -/
+theorem card_clippedRankPoints
+    (a b d : ℕ) (hd : d ≤ a + b - 1) :
+    (clippedRankPoints a b d).card = 2 * d := by
+  rw [clippedRankPoints, Finset.card_biUnion]
+  · simp [card_clipPair, mul_comm]
+  · exact clipPair_pairwise_disjoint a b d hd
+
+private theorem clipPair_subset_rankPatch
+    (a b c k : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hk : k < a + b - 1) :
+    clipPair a b k ⊆ rankPatch a b c := by
+  intro p hp
+  by_cases hkb : k < b
+  · simp [clipPair, hkb] at hp
+    rcases hp with rfl | rfl <;> rw [mem_rankPatch] <;>
+      simp [rankLevel] <;> omega
+  · have hbk : b ≤ k := Nat.le_of_not_gt hkb
+    simp [clipPair, hkb] at hp
+    rcases hp with rfl | rfl <;> rw [mem_rankPatch] <;>
+      simp [rankLevel] <;> omega
+
+/-- Every point removed by a valid clipping budget belongs to the original patch. -/
+theorem clippedRankPoints_subset_rankPatch
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hd : d ≤ a + b - 1) :
+    clippedRankPoints a b d ⊆ rankPatch a b c := by
+  intro p hp
+  rcases Finset.mem_biUnion.mp hp with ⟨k, hk, hpk⟩
+  exact clipPair_subset_rankPatch a b c k ha hb hc
+    (lt_of_lt_of_le (Finset.mem_range.mp hk) hd) hpk
+
+/-- Exact cardinality after `d` clipping steps. -/
+theorem card_clippedPatch
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hd : d ≤ a + b - 1) :
+    (clippedPatch a b c d).card = 2 * (a * b + b * c + c * a - d) := by
+  unfold clippedPatch
+  rw [Finset.card_image_of_injective _ rankPointVertex_injective,
+    Finset.card_sdiff_of_subset
+      (clippedRankPoints_subset_rankPatch a b c d ha hb hc hd),
+    card_rankPatch, card_clippedRankPoints a b d hd]
+  omega
+
+end OeisA263135
diff --git a/Scratch/A263135ClippingContacts.lean b/Scratch/A263135ClippingContacts.lean
new file mode 100644
index 0000000000..26a0a05d9f
--- /dev/null
+++ b/Scratch/A263135ClippingContacts.lean
@@ -0,0 +1,173 @@
+import Scratch.A263135RankDarts
+
+namespace OeisA263135
+
+@[simp]
+theorem rankPointVertex_mem_clippedPatch_iff
+    {a b c d : ℕ} {p : RankPoint} :
+    rankPointVertex p ∈ clippedPatch a b c d ↔
+      p ∈ rankPatch a b c ∧ p ∉ clippedRankPoints a b d := by
+  constructor
+  · intro hp
+    rcases Finset.mem_image.mp hp with ⟨q, hq, heq⟩
+    have hqp : q = p := rankPointVertex_injective heq
+    subst q
+    exact Finset.mem_sdiff.mp hq
+  · intro hp
+    exact Finset.mem_image.mpr ⟨p, Finset.mem_sdiff.mpr hp, rfl⟩
+
+/-- The clipped patch is a subset of the original convex patch. -/
+theorem clippedPatch_subset_patch (a b c d : ℕ) :
+    clippedPatch a b c d ⊆ patch a b c := by
+  intro v hv
+  rcases Finset.mem_image.mp hv with ⟨p, hp, rfl⟩
+  exact Finset.mem_image.mpr ⟨p, Finset.sdiff_subset hp, rfl⟩
+
+private theorem aInternalDarts_mono
+    {S T : Finset Vertex} (hST : S ⊆ T) :
+    aInternalDarts S ⊆ aInternalDarts T := by
+  intro vd hvd
+  rcases Finset.mem_filter.mp hvd with ⟨hint, hside⟩
+  rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+  rcases Finset.mem_product.mp hprod with ⟨hv, hd⟩
+  apply Finset.mem_filter.mpr
+  refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+    ⟨hST hv, hd⟩, hST hn⟩, hside⟩
+
+/-- Ranked contacts which survive all `d` clipping steps. -/
+def survivingPatchContactDarts (a b c d : ℕ) : Finset (RankPoint × Direction) :=
+  patchContactDarts a b c \ clippedLostDarts a b d
+
+private theorem rankDartNeighbor_mem_rankPatch
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {pd : RankPoint × Direction} (hpd : pd ∈ patchContactDarts a b c) :
+    rankDartNeighbor pd ∈ rankPatch a b c := by
+  have hint := (clippingRankDart_mem_aInternal_iff ha hb hc).mp hpd
+  rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+  rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+  rw [neighbor_clippingRankDart_eq hpd] at hn
+  exact rankPointVertex_mem_patch_iff.mp hn
+
+/-- For a contact of the original patch, survival is equivalent to both endpoints
+remaining after clipping. -/
+theorem clippingRankDart_mem_clipped_iff
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {pd : RankPoint × Direction} (hpd : pd ∈ patchContactDarts a b c) :
+    clippingRankDartVertex pd ∈ aInternalDarts (clippedPatch a b c d) ↔
+      pd.1 ∉ clippedRankPoints a b d ∧
+        rankDartNeighbor pd ∉ clippedRankPoints a b d := by
+  have hpPatch : pd.1 ∈ rankPatch a b c := by
+    have hint := (clippingRankDart_mem_aInternal_iff ha hb hc).mp hpd
+    rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+    rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+    exact rankPointVertex_mem_patch_iff.mp (Finset.mem_product.mp hprod).1
+  have hnPatch := rankDartNeighbor_mem_rankPatch ha hb hc hpd
+  constructor
+  · intro hint
+    rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+    rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+    have hpClip := (rankPointVertex_mem_clippedPatch_iff.mp
+      (Finset.mem_product.mp hprod).1).2
+    rw [neighbor_clippingRankDart_eq hpd] at hn
+    have hnClip := (rankPointVertex_mem_clippedPatch_iff.mp hn).2
+    exact ⟨hpClip, hnClip⟩
+  · rintro ⟨hpClip, hnClip⟩
+    apply Finset.mem_filter.mpr
+    refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+      ⟨rankPointVertex_mem_clippedPatch_iff.mpr ⟨hpPatch, hpClip⟩,
+        Finset.mem_univ _⟩, ?_⟩, ?_⟩
+    · rw [neighbor_clippingRankDart_eq hpd]
+      exact rankPointVertex_mem_clippedPatch_iff.mpr ⟨hnPatch, hnClip⟩
+    · have hfull := (clippingRankDart_mem_aInternal_iff ha hb hc).mp hpd
+      exact (Finset.mem_filter.mp hfull).2
+
+/-- The surviving ranked contacts are exactly the A-based internal darts of the
+clipped concrete patch. -/
+theorem surviving_mem_aInternal_iff
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hd : d ≤ a + b - 1)
+    {pd : RankPoint × Direction} :
+    pd ∈ survivingPatchContactDarts a b c d ↔
+      clippingRankDartVertex pd ∈ aInternalDarts (clippedPatch a b c d) := by
+  constructor
+  · intro hsurvive
+    rcases Finset.mem_sdiff.mp hsurvive with ⟨hpd, hnotLost⟩
+    apply (clippingRankDart_mem_clipped_iff a b c d ha hb hc hpd).mpr
+    have hnotEndpoints :
+        ¬(pd.1 ∈ clippedRankPoints a b d ∨
+          rankDartNeighbor pd ∈ clippedRankPoints a b d) := by
+      intro h
+      exact hnotLost ((mem_clippedLostDarts_iff a b c d ha hb hc hab hd hpd).mpr h)
+    exact not_or.mp hnotEndpoints
+  · intro hint
+    have hfull := aInternalDarts_mono (clippedPatch_subset_patch a b c d) hint
+    have hpd : pd ∈ patchContactDarts a b c :=
+      (clippingRankDart_mem_aInternal_iff ha hb hc).mpr hfull
+    apply Finset.mem_sdiff.mpr
+    refine ⟨hpd, ?_⟩
+    have hendpoints :=
+      (clippingRankDart_mem_clipped_iff a b c d ha hb hc hpd).mp hint
+    intro hlost
+    have h := (mem_clippedLostDarts_iff a b c d ha hb hc hab hd hpd).mp hlost
+    exact (not_or.mpr hendpoints) h
+
+/-- The ranked patch-contact list has cardinality equal to the original contact count. -/
+theorem card_patchContactDarts_eq_contacts
+    (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (patchContactDarts a b c).card = contacts (patch a b c) := by
+  rw [contacts_eq_card_aInternalDarts]
+  apply Finset.card_bij (fun pd hpd => clippingRankDartVertex pd)
+  · exact fun pd hpd => (clippingRankDart_mem_aInternal_iff ha hb hc).mp hpd
+  · intro p hp q hq h
+    exact clippingRankDartVertex_injective h
+  · intro vd hvd
+    rcases vd with ⟨v, direction⟩
+    rcases Finset.mem_filter.mp hvd with ⟨hint, hside⟩
+    rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+    rcases Finset.mem_image.mp (Finset.mem_product.mp hprod).1 with ⟨p, hp, rfl⟩
+    refine ⟨(p, direction), (clippingRankDart_mem_aInternal_iff ha hb hc).mpr ?_, rfl⟩
+    exact Finset.mem_filter.mpr ⟨hint, hside⟩
+
+/-- Contact count of a clipped patch is the number of surviving ranked darts. -/
+theorem contacts_clippedPatch_eq_card_surviving
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hd : d ≤ a + b - 1) :
+    contacts (clippedPatch a b c d) =
+      (survivingPatchContactDarts a b c d).card := by
+  rw [contacts_eq_card_aInternalDarts]
+  symm
+  apply Finset.card_bij (fun pd hpd => clippingRankDartVertex pd)
+  · exact fun pd hpd =>
+      (surviving_mem_aInternal_iff a b c d ha hb hc hab hd).mp hpd
+  · intro p hp q hq h
+    exact clippingRankDartVertex_injective h
+  · intro vd hvd
+    rcases vd with ⟨v, direction⟩
+    rcases Finset.mem_filter.mp hvd with ⟨hint, hside⟩
+    rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+    rcases Finset.mem_image.mp (Finset.mem_product.mp hprod).1 with ⟨p, hp, rfl⟩
+    refine ⟨(p, direction), ?_, rfl⟩
+    exact (surviving_mem_aInternal_iff a b c d ha hb hc hab hd).mpr
+      (Finset.mem_filter.mpr ⟨hint, hside⟩)
+
+/-- Exact contact count after `d` valid clipping steps. -/
+theorem contacts_clippedPatch_formula
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hd : d ≤ a + b - 1) :
+    contacts (clippedPatch a b c d) =
+      3 * (a * b + b * c + c * a - d) - (a + b + c) := by
+  have hlost_le := Finset.card_le_card
+    (clippedLostDarts_subset_patchContactDarts a b c d ha hb hc hab hd)
+  rw [card_clippedLostDarts a b d hd,
+    card_patchContactDarts_eq_contacts a b c ha hb hc,
+    contacts_patch_formula a b c ha hb hc] at hlost_le
+  rw [contacts_clippedPatch_eq_card_surviving a b c d ha hb hc hab hd]
+  unfold survivingPatchContactDarts
+  rw [Finset.card_sdiff_of_subset
+    (clippedLostDarts_subset_patchContactDarts a b c d ha hb hc hab hd),
+    card_clippedLostDarts a b d hd,
+    card_patchContactDarts_eq_contacts a b c ha hb hc,
+    contacts_patch_formula a b c ha hb hc]
+  omega
+
+end OeisA263135
diff --git a/Scratch/A263135ClippingDarts.lean b/Scratch/A263135ClippingDarts.lean
new file mode 100644
index 0000000000..30c2b18bfb
--- /dev/null
+++ b/Scratch/A263135ClippingDarts.lean
@@ -0,0 +1,104 @@
+import Scratch.A263135ClippingCard
+
+namespace OeisA263135
+
+/-- B-side point removed at clipping step `k`. -/
+def clipBPoint (a b k : ℕ) : RankPoint :=
+  if k < b then
+    ⟨k, b - 1 - k, true⟩
+  else
+    let h := k - b
+    ⟨h, b - h, true⟩
+
+/-- A-side point removed at clipping step `k`. -/
+def clipAPoint (a b k : ℕ) : RankPoint :=
+  if k < b then
+    ⟨k, b - k, false⟩
+  else
+    let h := k - b
+    ⟨h, b + 1 - h, false⟩
+
+/-- The A-side point immediately forward of the removed B point. -/
+def clipForwardAPoint (a b k : ℕ) : RankPoint :=
+  if k < b then
+    ⟨k + 1, b - 1 - k, false⟩
+  else
+    let h := k - b
+    ⟨h + 1, b - h, false⟩
+
+@[simp]
+theorem clipPair_eq (a b k : ℕ) :
+    clipPair a b k = {clipBPoint a b k, clipAPoint a b k} := by
+  unfold clipPair clipBPoint clipAPoint
+  split_ifs <;> rfl
+
+/-- The three A-based internal darts destroyed by clipping pair `k`.
+
+They are the same and diagonal darts based at the removed A point, together
+with the horizontal dart entering the removed B point from the forward A point.
+-/
+def clipLostDarts (a b k : ℕ) : Finset (RankPoint × Direction) :=
+  {(clipAPoint a b k, .same),
+    (clipAPoint a b k, .diagonal),
+    (clipForwardAPoint a b k, .horizontal)}
+
+@[simp]
+theorem card_clipLostDarts (a b k : ℕ) :
+    (clipLostDarts a b k).card = 3 := by
+  simp [clipLostDarts]
+
+private theorem clipAPoint_injective_on
+    {a b k l : ℕ} (hk : k < a + b - 1) (hl : l < a + b - 1)
+    (h : clipAPoint a b k = clipAPoint a b l) : k = l := by
+  by_cases hkb : k < b <;> by_cases hlb : l < b <;>
+    simp [clipAPoint, hkb, hlb] at h <;> omega
+
+private theorem clipForwardAPoint_injective_on
+    {a b k l : ℕ} (hk : k < a + b - 1) (hl : l < a + b - 1)
+    (h : clipForwardAPoint a b k = clipForwardAPoint a b l) : k = l := by
+  by_cases hkb : k < b <;> by_cases hlb : l < b <;>
+    simp [clipForwardAPoint, hkb, hlb] at h <;> omega
+
+private theorem clipLostDarts_pairwise_disjoint
+    (a b d : ℕ) (hd : d ≤ a + b - 1) :
+    (Finset.range d).toSet.PairwiseDisjoint (clipLostDarts a b) := by
+  intro k hk l hl hkl
+  have hkd : k < a + b - 1 := lt_of_lt_of_le (Finset.mem_range.mp hk) hd
+  have hld : l < a + b - 1 := lt_of_lt_of_le (Finset.mem_range.mp hl) hd
+  rw [Finset.disjoint_left]
+  intro pd hpk hpl
+  simp only [clipLostDarts, Finset.mem_insert, Finset.mem_singleton] at hpk hpl
+  rcases hpk with hpk | hpk | hpk <;>
+    rcases hpl with hpl | hpl | hpl
+  · exact hkl (clipAPoint_injective_on hkd hld
+      (congrArg Prod.fst (hpk.symm.trans hpl)))
+  · have := congrArg Prod.snd (hpk.symm.trans hpl)
+    simp at this
+  · have := congrArg Prod.snd (hpk.symm.trans hpl)
+    simp at this
+  · have := congrArg Prod.snd (hpk.symm.trans hpl)
+    simp at this
+  · exact hkl (clipAPoint_injective_on hkd hld
+      (congrArg Prod.fst (hpk.symm.trans hpl)))
+  · have := congrArg Prod.snd (hpk.symm.trans hpl)
+    simp at this
+  · have := congrArg Prod.snd (hpk.symm.trans hpl)
+    simp at this
+  · have := congrArg Prod.snd (hpk.symm.trans hpl)
+    simp at this
+  · exact hkl (clipForwardAPoint_injective_on hkd hld
+      (congrArg Prod.fst (hpk.symm.trans hpl)))
+
+/-- All A-based contact darts destroyed by the first `d` clipping steps. -/
+def clippedLostDarts (a b d : ℕ) : Finset (RankPoint × Direction) :=
+  (Finset.range d).biUnion fun k => clipLostDarts a b k
+
+/-- Exactly three distinct contact darts are destroyed per clipping pair. -/
+theorem card_clippedLostDarts
+    (a b d : ℕ) (hd : d ≤ a + b - 1) :
+    (clippedLostDarts a b d).card = 3 * d := by
+  rw [clippedLostDarts, Finset.card_biUnion]
+  · simp [card_clipLostDarts, mul_comm]
+  · exact clipLostDarts_pairwise_disjoint a b d hd
+
+end OeisA263135
diff --git a/Scratch/A263135ClippingGeometry.lean b/Scratch/A263135ClippingGeometry.lean
new file mode 100644
index 0000000000..7b03277f77
--- /dev/null
+++ b/Scratch/A263135ClippingGeometry.lean
@@ -0,0 +1,317 @@
+import Scratch.A263135ClippingDarts
+
+namespace OeisA263135
+
+/-- Ranked B endpoint of a ranked A-based dart. -/
+def rankDartNeighbor : RankPoint × Direction → RankPoint
+  | (p, .same) => sameRankNeighbor p
+  | (p, .horizontal) => horizontalRankNeighbor p
+  | (p, .diagonal) => diagonalRankNeighbor p
+
+@[simp]
+theorem clipBPoint_side (a b k : ℕ) : (clipBPoint a b k).side = true := by
+  unfold clipBPoint
+  split_ifs <;> rfl
+
+@[simp]
+theorem clipAPoint_side (a b k : ℕ) : (clipAPoint a b k).side = false := by
+  unfold clipAPoint
+  split_ifs <;> rfl
+
+@[simp]
+theorem clipForwardAPoint_side (a b k : ℕ) :
+    (clipForwardAPoint a b k).side = false := by
+  unfold clipForwardAPoint
+  split_ifs <;> rfl
+
+@[simp]
+theorem rankDartNeighbor_side (pd : RankPoint × Direction) :
+    (rankDartNeighbor pd).side = true := by
+  rcases pd with ⟨p, d⟩
+  cases d <;> rfl
+
+@[simp]
+theorem rankDartNeighbor_clipA_diagonal (a b k : ℕ) :
+    rankDartNeighbor (clipAPoint a b k, .diagonal) = clipBPoint a b k := by
+  by_cases hkb : k < b
+  · apply RankPoint.ext <;>
+      simp [rankDartNeighbor, diagonalRankNeighbor, clipAPoint, clipBPoint, hkb] <;> omega
+  · apply RankPoint.ext <;>
+      simp [rankDartNeighbor, diagonalRankNeighbor, clipAPoint, clipBPoint, hkb] <;> omega
+
+@[simp]
+theorem rankDartNeighbor_clipForward_horizontal (a b k : ℕ) :
+    rankDartNeighbor (clipForwardAPoint a b k, .horizontal) = clipBPoint a b k := by
+  by_cases hkb : k < b
+  · apply RankPoint.ext <;>
+      simp [rankDartNeighbor, horizontalRankNeighbor, clipForwardAPoint, clipBPoint, hkb] <;> omega
+  · apply RankPoint.ext <;>
+      simp [rankDartNeighbor, horizontalRankNeighbor, clipForwardAPoint, clipBPoint, hkb] <;> omega
+
+/-- Membership in the union of the first `d` clipping pairs. -/
+theorem mem_clippedRankPoints_iff {a b d : ℕ} {p : RankPoint} :
+    p ∈ clippedRankPoints a b d ↔
+      ∃ k < d, p = clipBPoint a b k ∨ p = clipAPoint a b k := by
+  constructor
+  · intro hp
+    rcases Finset.mem_biUnion.mp hp with ⟨k, hk, hpk⟩
+    have hk' : k < d := Finset.mem_range.mp hk
+    rw [clipPair_eq] at hpk
+    simpa only [Finset.mem_insert, Finset.mem_singleton] using ⟨k, hk', hpk⟩
+  · rintro ⟨k, hk, hpk⟩
+    apply Finset.mem_biUnion.mpr
+    refine ⟨k, Finset.mem_range.mpr hk, ?_⟩
+    rw [clipPair_eq]
+    simpa only [Finset.mem_insert, Finset.mem_singleton] using hpk
+
+private theorem clipAPoint_mem_aRankPatch
+    (a b c k : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hk : k < a + b - 1) :
+    clipAPoint a b k ∈ aRankPatch a b c := by
+  apply Finset.mem_filter.mpr
+  constructor
+  · rw [mem_rankPatch]
+    by_cases hkb : k < b <;>
+      simp [clipAPoint, rankLevel, hkb] <;> omega
+  · exact clipAPoint_side a b k
+
+private theorem clipForwardAPoint_mem_aRankPatch
+    (a b c k : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hk : k < a + b - 1) :
+    clipForwardAPoint a b k ∈ aRankPatch a b c := by
+  apply Finset.mem_filter.mpr
+  constructor
+  · rw [mem_rankPatch]
+    by_cases hkb : k < b <;>
+      simp [clipForwardAPoint, rankLevel, hkb] <;> omega
+  · exact clipForwardAPoint_side a b k
+
+private theorem clipAPoint_rankLevel_ne_top
+    (a b c k : ℕ) (ha : 0 < a) (hc : 0 < c)
+    (hk : k < a + b - 1) :
+    rankLevel (clipAPoint a b k) ≠ a + b + c - 1 := by
+  by_cases hkb : k < b <;>
+    simp [clipAPoint, rankLevel, hkb] <;> omega
+
+private theorem clipAPoint_second_ne_zero
+    (a b k : ℕ) (ha : 0 < a) (hb : 0 < b) (hab : a ≤ b)
+    (hk : k < a + b - 1) :
+    (clipAPoint a b k).second ≠ 0 := by
+  by_cases hkb : k < b <;>
+    simp [clipAPoint, hkb] <;> omega
+
+private theorem clipForwardAPoint_first_ne_zero (a b k : ℕ) :
+    (clipForwardAPoint a b k).first ≠ 0 := by
+  by_cases hkb : k < b <;>
+    simp [clipForwardAPoint, hkb]
+
+/-- Every explicitly listed lost dart was an internal patch contact before clipping. -/
+theorem clipLostDarts_subset_patchContactDarts
+    (a b c k : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hk : k < a + b - 1) :
+    clipLostDarts a b k ⊆ patchContactDarts a b c := by
+  intro pd hpd
+  simp only [clipLostDarts, Finset.mem_insert, Finset.mem_singleton] at hpd
+  rcases hpd with rfl | rfl | rfl
+  · have hp := clipAPoint_mem_aRankPatch a b c k ha hb hc hab hk
+    have htop := clipAPoint_rankLevel_ne_top a b c k ha hc hk
+    simp [patchContactDarts, sameContactPoints, hp, htop]
+  · have hp := clipAPoint_mem_aRankPatch a b c k ha hb hc hab hk
+    have hsecond := clipAPoint_second_ne_zero a b k ha hb hab hk
+    simp [patchContactDarts, diagonalContactPoints, hp, hsecond]
+  · have hp := clipForwardAPoint_mem_aRankPatch a b c k ha hb hc hab hk
+    have hfirst := clipForwardAPoint_first_ne_zero a b k
+    simp [patchContactDarts, horizontalContactPoints, hp, hfirst]
+
+/-- Every lost dart from a valid clipping budget is a contact of the original patch. -/
+theorem clippedLostDarts_subset_patchContactDarts
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hd : d ≤ a + b - 1) :
+    clippedLostDarts a b d ⊆ patchContactDarts a b c := by
+  intro pd hpd
+  rcases Finset.mem_biUnion.mp hpd with ⟨k, hk, hpdk⟩
+  exact clipLostDarts_subset_patchContactDarts a b c k ha hb hc hab
+    (lt_of_lt_of_le (Finset.mem_range.mp hk) hd) hpdk
+
+private theorem clipA_horizontal_eq_forward_pred
+    (a b k : ℕ) (hk : 0 < k) (htrans : k ≠ b) :
+    clipAPoint a b k = clipForwardAPoint a b (k - 1) := by
+  by_cases hkb : k < b
+  · have hpred : k - 1 < b := by omega
+    apply RankPoint.ext <;>
+      simp [clipAPoint, clipForwardAPoint, hkb, hpred] <;> omega
+  · have hpred : ¬ k - 1 < b := by omega
+    apply RankPoint.ext <;>
+      simp [clipAPoint, clipForwardAPoint, hkb, hpred] <;> omega
+
+private theorem same_base_of_clipB
+    {a b k : ℕ} {p : RankPoint}
+    (h : rankDartNeighbor (p, .same) = clipBPoint a b k) :
+    p.first = (clipBPoint a b k).first ∧
+      p.second = (clipBPoint a b k).second := by
+  simpa [rankDartNeighbor, sameRankNeighbor] using congrArg
+    (fun q : RankPoint => (q.first, q.second)) h
+
+private theorem horizontal_base_of_clipB
+    {a b k : ℕ} {p : RankPoint} (hpSide : p.side = false) (hp : p.first ≠ 0)
+    (h : rankDartNeighbor (p, .horizontal) = clipBPoint a b k) :
+    p = clipForwardAPoint a b k := by
+  by_cases hkb : k < b
+  · apply RankPoint.ext
+    · have hf := congrArg RankPoint.first h
+      simp [rankDartNeighbor, horizontalRankNeighbor, clipBPoint,
+        clipForwardAPoint, hkb] at hf ⊢
+      omega
+    · have hs := congrArg RankPoint.second h
+      simpa [rankDartNeighbor, horizontalRankNeighbor, clipBPoint,
+        clipForwardAPoint, hkb] using hs
+    · exact hpSide.trans (clipForwardAPoint_side a b k).symm
+  · apply RankPoint.ext
+    · have hf := congrArg RankPoint.first h
+      simp [rankDartNeighbor, horizontalRankNeighbor, clipBPoint,
+        clipForwardAPoint, hkb] at hf ⊢
+      omega
+    · have hs := congrArg RankPoint.second h
+      simpa [rankDartNeighbor, horizontalRankNeighbor, clipBPoint,
+        clipForwardAPoint, hkb] using hs
+    · exact hpSide.trans (clipForwardAPoint_side a b k).symm
+
+private theorem diagonal_base_of_clipB
+    {a b k : ℕ} {p : RankPoint} (hpSide : p.side = false) (hp : p.second ≠ 0)
+    (h : rankDartNeighbor (p, .diagonal) = clipBPoint a b k) :
+    p = clipAPoint a b k := by
+  by_cases hkb : k < b
+  · apply RankPoint.ext
+    · have hf := congrArg RankPoint.first h
+      simpa [rankDartNeighbor, diagonalRankNeighbor, clipBPoint,
+        clipAPoint, hkb] using hf
+    · have hs := congrArg RankPoint.second h
+      simp [rankDartNeighbor, diagonalRankNeighbor, clipBPoint,
+        clipAPoint, hkb] at hs ⊢
+      omega
+    · exact hpSide.trans (clipAPoint_side a b k).symm
+  · apply RankPoint.ext
+    · have hf := congrArg RankPoint.first h
+      simpa [rankDartNeighbor, diagonalRankNeighbor, clipBPoint,
+        clipAPoint, hkb] using hf
+    · have hs := congrArg RankPoint.second h
+      simp [rankDartNeighbor, diagonalRankNeighbor, clipBPoint,
+        clipAPoint, hkb] at hs ⊢
+      omega
+    · exact hpSide.trans (clipAPoint_side a b k).symm
+
+private theorem patchContactDart_base_side
+    {a b c : ℕ} {pd : RankPoint × Direction}
+    (hpd : pd ∈ patchContactDarts a b c) : pd.1.side = false := by
+  rcases pd with ⟨p, direction⟩
+  cases direction
+  · have hp : p ∈ sameContactPoints a b c := by
+      simpa [patchContactDarts] using hpd
+    exact (Finset.mem_filter.mp (Finset.mem_filter.mp hp).1).2
+  · have hp : p ∈ horizontalContactPoints a b c := by
+      simpa [patchContactDarts] using hpd
+    exact (Finset.mem_filter.mp (Finset.mem_filter.mp hp).1).2
+  · have hp : p ∈ diagonalContactPoints a b c := by
+      simpa [patchContactDarts] using hpd
+    exact (Finset.mem_filter.mp (Finset.mem_filter.mp hp).1).2
+
+/-- A patch contact is destroyed by clipping exactly when one of its endpoints is clipped. -/
+theorem mem_clippedLostDarts_iff
+    (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : a ≤ b) (hd : d ≤ a + b - 1)
+    {pd : RankPoint × Direction} (hpd : pd ∈ patchContactDarts a b c) :
+    pd ∈ clippedLostDarts a b d ↔
+      pd.1 ∈ clippedRankPoints a b d ∨
+        rankDartNeighbor pd ∈ clippedRankPoints a b d := by
+  constructor
+  · intro hlost
+    rcases Finset.mem_biUnion.mp hlost with ⟨k, hk, hpdk⟩
+    have hk' : k < d := Finset.mem_range.mp hk
+    simp only [clipLostDarts, Finset.mem_insert, Finset.mem_singleton] at hpdk
+    rcases hpdk with rfl | rfl | rfl
+    · left
+      exact mem_clippedRankPoints_iff.mpr ⟨k, hk', Or.inr rfl⟩
+    · left
+      exact mem_clippedRankPoints_iff.mpr ⟨k, hk', Or.inr rfl⟩
+    · right
+      rw [rankDartNeighbor_clipForward_horizontal]
+      exact mem_clippedRankPoints_iff.mpr ⟨k, hk', Or.inl rfl⟩
+  · rintro (hbase | hneighbor)
+    · have hbaseSide := patchContactDart_base_side hpd
+      rcases mem_clippedRankPoints_iff.mp hbase with ⟨k, hk, hpk | hpk⟩
+      · have hs := congrArg RankPoint.side hpk
+        rw [hbaseSide] at hs
+        simp at hs
+      · rcases pd with ⟨p, direction⟩
+        subst p
+        apply Finset.mem_biUnion.mpr
+        cases direction
+        · exact ⟨k, Finset.mem_range.mpr hk, by simp [clipLostDarts]⟩
+        · have hpHorizontal : clipAPoint a b k ∈ horizontalContactPoints a b c := by
+            simpa [patchContactDarts] using hpd
+          have hfirst : (clipAPoint a b k).first ≠ 0 :=
+            (Finset.mem_filter.mp hpHorizontal).2
+          have hkpos : 0 < k := by
+            by_cases hkb : k < b <;> simp [clipAPoint, hkb] at hfirst <;> omega
+          have htrans : k ≠ b := by
+            intro hkb
+            subst k
+            simp [clipAPoint] at hfirst
+          have hpred : k - 1 < d := by omega
+          refine ⟨k - 1, Finset.mem_range.mpr hpred, ?_⟩
+          have heq := clipA_horizontal_eq_forward_pred a b k hkpos htrans
+          simp [clipLostDarts, heq]
+        · exact ⟨k, Finset.mem_range.mpr hk, by simp [clipLostDarts]⟩
+    · rcases mem_clippedRankPoints_iff.mp hneighbor with ⟨k, hk, hpk | hpk⟩
+      · rcases pd with ⟨p, direction⟩
+        cases direction
+        · have hpSame : p ∈ sameContactPoints a b c := by
+            simpa [patchContactDarts] using hpd
+          have hpA := (Finset.mem_filter.mp hpSame).1
+          have hpSide := (Finset.mem_filter.mp hpA).2
+          have hcoords := same_base_of_clipB hpk
+          by_cases hkb : k < b
+          · have hpPatch := (Finset.mem_filter.mp hpA).1
+            rw [mem_rankPatch] at hpPatch
+            have hfirst := hcoords.1
+            have hsecond := hcoords.2
+            simp [clipBPoint, hkb] at hfirst hsecond
+            rcases p with ⟨i, j, side⟩
+            simp [rankLevel] at hpSide hpPatch
+            omega
+          · let h := k - b
+            have hkmax : k < a + b - 1 := lt_of_lt_of_le hk hd
+            have hh : h < b := by
+              dsimp [h]
+              omega
+            have hpEq : p = clipAPoint a b h := by
+              apply RankPoint.ext
+              · simpa [clipAPoint, hh, clipBPoint, hkb, h] using hcoords.1
+              · simpa [clipAPoint, hh, clipBPoint, hkb, h] using hcoords.2
+              · exact hpSide.trans (clipAPoint_side a b h).symm
+            have hhd : h < d := by dsimp [h]; omega
+            subst p
+            exact Finset.mem_biUnion.mpr
+              ⟨h, Finset.mem_range.mpr hhd, by simp [clipLostDarts]⟩
+        · have hpHorizontal : p ∈ horizontalContactPoints a b c := by
+            simpa [patchContactDarts] using hpd
+          have hpA := (Finset.mem_filter.mp hpHorizontal).1
+          have hpSide := (Finset.mem_filter.mp hpA).2
+          have hfirst := (Finset.mem_filter.mp hpHorizontal).2
+          have hpEq := horizontal_base_of_clipB hpSide hfirst hpk
+          subst p
+          exact Finset.mem_biUnion.mpr
+            ⟨k, Finset.mem_range.mpr hk, by simp [clipLostDarts]⟩
+        · have hpDiagonal : p ∈ diagonalContactPoints a b c := by
+            simpa [patchContactDarts] using hpd
+          have hpA := (Finset.mem_filter.mp hpDiagonal).1
+          have hpSide := (Finset.mem_filter.mp hpA).2
+          have hsecond := (Finset.mem_filter.mp hpDiagonal).2
+          have hpEq := diagonal_base_of_clipB hpSide hsecond hpk
+          subst p
+          exact Finset.mem_biUnion.mpr
+            ⟨k, Finset.mem_range.mpr hk, by simp [clipLostDarts]⟩
+      · have hs := congrArg RankPoint.side hpk
+        simp [rankDartNeighbor_side] at hs
+
+end OeisA263135
diff --git a/Scratch/A263135Endpoints.lean b/Scratch/A263135Endpoints.lean
new file mode 100644
index 0000000000..a8310e4326
--- /dev/null
+++ b/Scratch/A263135Endpoints.lean
@@ -0,0 +1,164 @@
+import Scratch.A263135Boundary
+
+namespace OeisA263135
+
+/-- Vertices of `S` lying on the row `x` of kind `r`. -/
+def rowSlice (r : RowKind) (S : Finset Vertex) (x : ℤ) : Finset Vertex :=
+  S.filter fun v => rowCoord r v = x
+
+private theorem rowSlice_nonempty (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) : (rowSlice r S x).Nonempty := by
+  rcases Finset.mem_image.mp x.property with ⟨v, hvS, hvx⟩
+  exact ⟨v, Finset.mem_filter.mpr ⟨hvS, hvx⟩⟩
+
+private theorem exists_min_vertex (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) :
+    ∃ v : Vertex,
+      v ∈ S ∧ rowCoord r v = x ∧
+        ∀ w ∈ S, rowCoord r w = x → alongCoord r v ≤ alongCoord r w := by
+  let T := rowSlice r S x
+  have hT : T.Nonempty := rowSlice_nonempty r S x
+  let A := T.image (alongCoord r)
+  have hA : A.Nonempty := hT.image _
+  have hm : A.min' hA ∈ A := A.min'_mem hA
+  rcases Finset.mem_image.mp hm with ⟨v, hvT, hv⟩
+  refine ⟨v, (Finset.mem_filter.mp hvT).1, (Finset.mem_filter.mp hvT).2, ?_⟩
+  intro w hwS hwx
+  have hwT : w ∈ T := Finset.mem_filter.mpr ⟨hwS, hwx⟩
+  have hwA : alongCoord r w ∈ A := Finset.mem_image.mpr ⟨w, hwT, rfl⟩
+  have hle := A.min'_le (alongCoord r w) hwA
+  simpa [hv] using hle
+
+private theorem exists_max_vertex (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) :
+    ∃ v : Vertex,
+      v ∈ S ∧ rowCoord r v = x ∧
+        ∀ w ∈ S, rowCoord r w = x → alongCoord r w ≤ alongCoord r v := by
+  let T := rowSlice r S x
+  have hT : T.Nonempty := rowSlice_nonempty r S x
+  let A := T.image (alongCoord r)
+  have hA : A.Nonempty := hT.image _
+  have hm : A.max' hA ∈ A := A.max'_mem hA
+  rcases Finset.mem_image.mp hm with ⟨v, hvT, hv⟩
+  refine ⟨v, (Finset.mem_filter.mp hvT).1, (Finset.mem_filter.mp hvT).2, ?_⟩
+  intro w hwS hwx
+  have hwT : w ∈ T := Finset.mem_filter.mpr ⟨hwS, hwx⟩
+  have hwA : alongCoord r w ∈ A := Finset.mem_image.mpr ⟨w, hwT, rfl⟩
+  have hle := A.le_max' (alongCoord r w) hwA
+  simpa [hv] using hle
+
+noncomputable def minRowVertex (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) : Vertex :=
+  Classical.choose (exists_min_vertex r S x)
+
+noncomputable def maxRowVertex (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) : Vertex :=
+  Classical.choose (exists_max_vertex r S x)
+
+private theorem minRowVertex_spec (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) :
+    minRowVertex r S x ∈ S ∧ rowCoord r (minRowVertex r S x) = x ∧
+      ∀ w ∈ S, rowCoord r w = x →
+        alongCoord r (minRowVertex r S x) ≤ alongCoord r w :=
+  Classical.choose_spec (exists_min_vertex r S x)
+
+private theorem maxRowVertex_spec (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) :
+    maxRowVertex r S x ∈ S ∧ rowCoord r (maxRowVertex r S x) = x ∧
+      ∀ w ∈ S, rowCoord r w = x →
+        alongCoord r w ≤ alongCoord r (maxRowVertex r S x) :=
+  Classical.choose_spec (exists_max_vertex r S x)
+
+private theorem prev_minRowVertex_not_mem (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) :
+    neighbor (minRowVertex r S x) (prevDirection r (minRowVertex r S x)) ∉ S := by
+  intro hmem
+  have hmin := (minRowVertex_spec r S x).2.2 _ hmem (by simp)
+  rw [alongCoord_neighbor_prev] at hmin
+  omega
+
+private theorem next_maxRowVertex_not_mem (r : RowKind) (S : Finset Vertex)
+    (x : ↥(occupiedRows r S)) :
+    neighbor (maxRowVertex r S x) (nextDirection r (maxRowVertex r S x)) ∉ S := by
+  intro hmem
+  have hmax := (maxRowVertex_spec r S x).2.2 _ hmem (by simp)
+  rw [alongCoord_neighbor_next] at hmax
+  omega
+
+/-- The lower or upper outgoing dart associated to an occupied row. -/
+noncomputable def endpointDart (r : RowKind) (S : Finset Vertex)
+    (xb : ↥(occupiedRows r S) × Bool) : Vertex × Direction :=
+  if xb.2 then
+    let v := maxRowVertex r S xb.1
+    (v, nextDirection r v)
+  else
+    let v := minRowVertex r S xb.1
+    (v, prevDirection r v)
+
+private theorem endpointDart_mem (r : RowKind) (S : Finset Vertex)
+    (xb : ↥(occupiedRows r S) × Bool) : endpointDart r S xb ∈ rowBoundaryDarts r S := by
+  classical
+  rcases xb with ⟨x, side⟩
+  cases side
+  · simp only [endpointDart, Bool.false_eq_true, ↓reduceIte]
+    let v := minRowVertex r S x
+    have hvS : v ∈ S := (minRowVertex_spec r S x).1
+    have hout : neighbor v (prevDirection r v) ∉ S := prev_minRowVertex_not_mem r S x
+    have hrow : r ∈ preservedRows (v, prevDirection r v) := by
+      simp [preservedRows]
+    exact Finset.mem_filter.mpr
+      ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨hvS, Finset.mem_univ _⟩, hout⟩, hrow⟩
+  · simp only [endpointDart, ↓reduceIte]
+    let v := maxRowVertex r S x
+    have hvS : v ∈ S := (maxRowVertex_spec r S x).1
+    have hout : neighbor v (nextDirection r v) ∉ S := next_maxRowVertex_not_mem r S x
+    have hrow : r ∈ preservedRows (v, nextDirection r v) := by
+      simp [preservedRows]
+    exact Finset.mem_filter.mpr
+      ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨hvS, Finset.mem_univ _⟩, hout⟩, hrow⟩
+
+private theorem endpointDart_injective (r : RowKind) (S : Finset Vertex) :
+    Function.Injective (endpointDart r S) := by
+  intro a b hab
+  rcases a with ⟨x, sx⟩
+  rcases b with ⟨y, sy⟩
+  cases sx <;> cases sy
+  · apply Prod.ext
+    · apply Subtype.ext
+      have hv := congrArg (fun vd => rowCoord r vd.1) hab
+      simpa [endpointDart, (minRowVertex_spec r S x).2.1,
+        (minRowVertex_spec r S y).2.1] using hv
+    · rfl
+  · exfalso
+    have hv := congrArg Prod.fst hab
+    have hd := congrArg Prod.snd hab
+    simp only [endpointDart, Bool.false_eq_true, ↓reduceIte] at hv hd
+    rw [hv] at hd
+    exact prevDirection_ne_nextDirection r _ hd
+  · exfalso
+    have hv := congrArg Prod.fst hab
+    have hd := congrArg Prod.snd hab
+    simp only [endpointDart, Bool.false_eq_true, ↓reduceIte] at hv hd
+    rw [hv] at hd
+    exact prevDirection_ne_nextDirection r _ hd.symm
+  · apply Prod.ext
+    · apply Subtype.ext
+      have hv := congrArg (fun vd => rowCoord r vd.1) hab
+      simpa [endpointDart, (maxRowVertex_spec r S x).2.1,
+        (maxRowVertex_spec r S y).2.1] using hv
+    · rfl
+
+/-- Every occupied row contributes two distinct boundary darts. -/
+theorem two_mul_occupiedRows_card_le_rowBoundaryDarts_card
+    (r : RowKind) (S : Finset Vertex) :
+    2 * (occupiedRows r S).card ≤ (rowBoundaryDarts r S).card := by
+  classical
+  let f : (↥(occupiedRows r S) × Bool) → ↥(rowBoundaryDarts r S) :=
+    fun xb => ⟨endpointDart r S xb, endpointDart_mem r S xb⟩
+  have hf : Function.Injective f := by
+    intro a b h
+    exact endpointDart_injective r S (Subtype.ext_iff.mp h)
+  have hcard := Fintype.card_le_of_injective f hf
+  simpa [f, mul_comm] using hcard
+
+end OeisA263135
diff --git a/Scratch/A263135Final.lean b/Scratch/A263135Final.lean
new file mode 100644
index 0000000000..8e848c22c0
--- /dev/null
+++ b/Scratch/A263135Final.lean
@@ -0,0 +1,56 @@
+import Scratch.A263135ClippingContacts
+
+namespace OeisA263135
+
+/-- The successor of the floor square root of `x-1` is the natural ceiling square root of positive
+`x`. -/
+theorem isNatCeilSqrt_pred_sqrt_succ (x : ℕ) (hx : 0 < x) :
+    IsNatCeilSqrt x ((x - 1).sqrt + 1) := by
+  constructor
+  · have hs := Nat.sqrt_le' (x - 1)
+    simp only [Nat.add_sub_cancel]
+    omega
+  · have hs := Nat.succ_le_succ_sqrt' (x - 1)
+    omega
+
+private def twoVertexWitness : Finset Vertex :=
+  {⟨0, 0, false⟩, ⟨0, 0, true⟩}
+
+@[simp]
+private theorem card_twoVertexWitness : twoVertexWitness.card = 2 := by
+  simp [twoVertexWitness]
+
+@[simp]
+private theorem contacts_twoVertexWitness : contacts twoVertexWitness = 1 := by
+  norm_num [twoVertexWitness, contacts, neighbor]
+
+/-- Complete even-index extremal theorem for OEIS A263135. -/
+@[category research solved, AMS 05]
+theorem conjecture_solved (n : ℕ) (hn : 0 < n) :
+    ∃ r : ℕ, IsNatCeilSqrt (3 * n) r ∧
+      IsMaximumContact (2 * n) (3 * n - r) := by
+  let r := (3 * n - 1).sqrt + 1
+  have hr : IsNatCeilSqrt (3 * n) r := by
+    exact isNatCeilSqrt_pred_sqrt_succ (3 * n) (by positivity)
+  refine ⟨r, hr, ?_⟩
+  constructor
+  · by_cases hn1 : n = 1
+    · subst n
+      refine ⟨twoVertexWitness, by simp, ?_⟩
+      have hr2 : r = 2 := by
+        dsimp [r]
+        norm_num
+      rw [hr2]
+      simp
+    · have hn2 : 1 < n := by omega
+      rcases exists_balanced_clipping_parameters n r hn2 hr with
+        ⟨a, b, c, d, ha, hb, hc, hab, hbc, hsum, hM, hd⟩
+      refine ⟨clippedPatch a b c d, ?_, ?_⟩
+      · rw [card_clippedPatch a b c d ha hb hc hd]
+        omega
+      · rw [contacts_clippedPatch_formula a b c d ha hb hc hab hd]
+        omega
+  · intro S hcard
+    exact contacts_le_even_closed_form S n r hcard hr
+
+end OeisA263135
diff --git a/Scratch/A263135Incidence.lean b/Scratch/A263135Incidence.lean
new file mode 100644
index 0000000000..d2c3565575
--- /dev/null
+++ b/Scratch/A263135Incidence.lean
@@ -0,0 +1,129 @@
+import Scratch.A263135Symmetry
+
+namespace OeisA263135
+
+/-- Directed honeycomb incidences whose two endpoints lie in `S`. -/
+def internalDarts (S : Finset Vertex) : Finset (Vertex × Direction) :=
+  (S ×ˢ Finset.univ).filter fun vd => neighbor vd.1 vd.2 ∈ S
+
+/-- Internal darts based at the `A` side. -/
+def aInternalDarts (S : Finset Vertex) : Finset (Vertex × Direction) :=
+  (internalDarts S).filter fun vd => vd.1.side = false
+
+/-- Internal darts based at the `B` side. -/
+def bInternalDarts (S : Finset Vertex) : Finset (Vertex × Direction) :=
+  (internalDarts S).filter fun vd => vd.1.side = true
+
+private theorem internal_boundary_disjoint (S : Finset Vertex) :
+    Disjoint (internalDarts S) (boundaryDarts S) := by
+  rw [Finset.disjoint_left]
+  intro vd hi hb
+  exact (Finset.mem_filter.mp hi).2 (Finset.mem_filter.mp hb).2
+
+private theorem internal_union_boundary (S : Finset Vertex) :
+    internalDarts S ∪ boundaryDarts S = S ×ˢ Finset.univ := by
+  ext vd
+  simp [internalDarts, boundaryDarts]
+
+/-- Every vertex has three directed incidences, split into internal and boundary darts. -/
+theorem card_internalDarts_add_edgeBoundary (S : Finset Vertex) :
+    (internalDarts S).card + edgeBoundary S = 3 * S.card := by
+  rw [edgeBoundary, ← Finset.card_union_of_disjoint (internal_boundary_disjoint S),
+    internal_union_boundary]
+  simp [mul_comm]
+
+private theorem a_b_internal_disjoint (S : Finset Vertex) :
+    Disjoint (aInternalDarts S) (bInternalDarts S) := by
+  rw [Finset.disjoint_left]
+  intro vd ha hb
+  have hfalse := (Finset.mem_filter.mp ha).2
+  have htrue := (Finset.mem_filter.mp hb).2
+  simp [hfalse] at htrue
+
+private theorem a_union_b_internal (S : Finset Vertex) :
+    aInternalDarts S ∪ bInternalDarts S = internalDarts S := by
+  ext vd
+  simp [aInternalDarts, bInternalDarts]
+  cases h : vd.1.side <;> simp [h]
+
+/-- Reversal of a directed honeycomb incidence. -/
+def reverseDart (vd : Vertex × Direction) : Vertex × Direction :=
+  (neighbor vd.1 vd.2, vd.2)
+
+@[simp]
+theorem reverseDart_involutive (vd : Vertex × Direction) :
+    reverseDart (reverseDart vd) = vd := by
+  rcases vd with ⟨v, d⟩
+  simp [reverseDart]
+
+private theorem reverseDart_injective : Function.Injective reverseDart :=
+  Function.LeftInverse.injective reverseDart_involutive
+
+private theorem reverse_a_mem_b (S : Finset Vertex) {vd : Vertex × Direction}
+    (h : vd ∈ aInternalDarts S) : reverseDart vd ∈ bInternalDarts S := by
+  rcases vd with ⟨v, d⟩
+  rcases Finset.mem_filter.mp h with ⟨hint, hvside⟩
+  rcases Finset.mem_filter.mp hint with ⟨hprod, hnmem⟩
+  rcases Finset.mem_product.mp hprod with ⟨hvS, hd⟩
+  apply Finset.mem_filter.mpr
+  constructor
+  · apply Finset.mem_filter.mpr
+    exact ⟨Finset.mem_product.mpr ⟨hnmem, hd⟩, by simpa⟩
+  · rcases v with ⟨i, j, side⟩
+    cases side <;> cases d <;> simp [reverseDart, neighbor] at hvside ⊢
+
+private theorem reverse_b_mem_a (S : Finset Vertex) {vd : Vertex × Direction}
+    (h : vd ∈ bInternalDarts S) : reverseDart vd ∈ aInternalDarts S := by
+  rcases vd with ⟨v, d⟩
+  rcases Finset.mem_filter.mp h with ⟨hint, hvside⟩
+  rcases Finset.mem_filter.mp hint with ⟨hprod, hnmem⟩
+  rcases Finset.mem_product.mp hprod with ⟨hvS, hd⟩
+  apply Finset.mem_filter.mpr
+  constructor
+  · apply Finset.mem_filter.mpr
+    exact ⟨Finset.mem_product.mpr ⟨hnmem, hd⟩, by simpa⟩
+  · rcases v with ⟨i, j, side⟩
+    cases side <;> cases d <;> simp [reverseDart, neighbor] at hvside ⊢
+
+/-- Internal darts based at the two bipartite sides are equinumerous. -/
+theorem card_aInternalDarts_eq_card_bInternalDarts (S : Finset Vertex) :
+    (aInternalDarts S).card = (bInternalDarts S).card := by
+  apply Nat.le_antisymm
+  · exact Finset.card_le_card_of_injOn reverseDart
+      (fun _ h => reverse_a_mem_b S h)
+      (fun _ _ _ _ h => reverseDart_injective h)
+  · exact Finset.card_le_card_of_injOn reverseDart
+      (fun _ h => reverse_b_mem_a S h)
+      (fun _ _ _ _ h => reverseDart_injective h)
+
+/-- The original `contacts` sum is the cardinality of the `A`-based internal darts. -/
+theorem contacts_eq_card_aInternalDarts (S : Finset Vertex) :
+    contacts S = (aInternalDarts S).card := by
+  classical
+  unfold contacts aInternalDarts internalDarts
+  rw [Finset.card_eq_sum_card_fiberwise
+    (s := ((S ×ˢ Finset.univ).filter fun vd => neighbor vd.1 vd.2 ∈ S).filter
+      fun vd => vd.1.side = false)
+    (g := Prod.fst) (t := S) (by simp)]
+  apply Finset.sum_congr rfl
+  intro v hv
+  cases hside : v.side
+  · simp [hside]
+  · simp [hside, Finset.card_eq_sum_ones]
+
+/-- The number of directed internal darts is twice the contact count. -/
+theorem card_internalDarts_eq_two_mul_contacts (S : Finset Vertex) :
+    (internalDarts S).card = 2 * contacts S := by
+  rw [← a_union_b_internal S,
+    Finset.card_union_of_disjoint (a_b_internal_disjoint S),
+    ← contacts_eq_card_aInternalDarts,
+    ← card_aInternalDarts_eq_card_bInternalDarts S]
+  omega
+
+/-- Incidence bookkeeping for every finite honeycomb set. -/
+theorem three_mul_card_eq_two_mul_contacts_add_boundary (S : Finset Vertex) :
+    3 * S.card = 2 * contacts S + edgeBoundary S := by
+  rw [← card_internalDarts_eq_two_mul_contacts]
+  omega
+
+end OeisA263135
diff --git a/Scratch/A263135Parameters.lean b/Scratch/A263135Parameters.lean
new file mode 100644
index 0000000000..7e3798d30e
--- /dev/null
+++ b/Scratch/A263135Parameters.lean
@@ -0,0 +1,129 @@
+import Scratch.A263135Upper
+
+namespace OeisA263135
+
+/-- Balanced side parameters for a perimeter parameter `r`. -/
+def balancedA (r : ℕ) : ℕ := r / 3
+
+def balancedB (r : ℕ) : ℕ := (r + 1) / 3
+
+def balancedC (r : ℕ) : ℕ := (r + 2) / 3
+
+/-- The three balanced parameters sum to `r`. -/
+theorem balanced_sum (r : ℕ) :
+    balancedA r + balancedB r + balancedC r = r := by
+  unfold balancedA balancedB balancedC
+  omega
+
+/-- The balanced parameters are weakly increasing. -/
+theorem balanced_order (r : ℕ) :
+    balancedA r ≤ balancedB r ∧ balancedB r ≤ balancedC r := by
+  unfold balancedA balancedB balancedC
+  omega
+
+/-- Pair-product sum of balanced parameters. -/
+theorem balanced_pair_sum (r : ℕ) :
+    balancedA r * balancedB r + balancedB r * balancedC r +
+      balancedC r * balancedA r = r ^ 2 / 3 := by
+  unfold balancedA balancedB balancedC
+  let q := r / 3
+  have hmod : r % 3 = 0 ∨ r % 3 = 1 ∨ r % 3 = 2 := by omega
+  rcases hmod with h | h | h
+  · have hr : r = 3 * q := by dsimp [q]; omega
+    have h0 : r / 3 = q := rfl
+    have h1 : (r + 1) / 3 = q := by dsimp [q]; omega
+    have h2 : (r + 2) / 3 = q := by dsimp [q]; omega
+    have hs : r ^ 2 / 3 = 3 * q ^ 2 := by
+      rw [hr]
+      ring_nf
+      omega
+    rw [h0, h1, h2, hs]
+    ring
+  · have hr : r = 3 * q + 1 := by dsimp [q]; omega
+    have h0 : r / 3 = q := rfl
+    have h1 : (r + 1) / 3 = q := by dsimp [q]; omega
+    have h2 : (r + 2) / 3 = q + 1 := by dsimp [q]; omega
+    have hs : r ^ 2 / 3 = 3 * q ^ 2 + 2 * q := by
+      rw [hr]
+      ring_nf
+      omega
+    rw [h0, h1, h2, hs]
+    ring
+  · have hr : r = 3 * q + 2 := by dsimp [q]; omega
+    have h0 : r / 3 = q := rfl
+    have h1 : (r + 1) / 3 = q + 1 := by dsimp [q]; omega
+    have h2 : (r + 2) / 3 = q + 1 := by dsimp [q]; omega
+    have hs : r ^ 2 / 3 = 3 * q ^ 2 + 4 * q + 1 := by
+      rw [hr]
+      ring_nf
+      omega
+    rw [h0, h1, h2, hs]
+    ring
+
+/-- Width of the available clipping corner. -/
+theorem balanced_corner_width (r : ℕ) (hr : 3 ≤ r) :
+    balancedA r + balancedB r - 1 =
+      r ^ 2 / 3 - (r - 1) ^ 2 / 3 - 1 := by
+  unfold balancedA balancedB
+  have hmod : r % 3 = 0 ∨ r % 3 = 1 ∨ r % 3 = 2 := by omega
+  rcases hmod with h | h | h
+  · have hre : r = 3 * (r / 3) := by omega
+    rw [hre]
+    ring_nf
+    omega
+  · have hre : r = 3 * (r / 3) + 1 := by omega
+    rw [hre]
+    ring_nf
+    omega
+  · have hre : r = 3 * (r / 3) + 2 := by omega
+    rw [hre]
+    ring_nf
+    omega
+
+/-- Positivity of the balanced side parameters once `r ≥ 3`. -/
+theorem balanced_positive (r : ℕ) (hr : 3 ≤ r) :
+    0 < balancedA r ∧ 0 < balancedB r ∧ 0 < balancedC r := by
+  unfold balancedA balancedB balancedC
+  omega
+
+/-- The ceiling-square interval supplies ordered balanced parameters and a valid clipping budget. -/
+theorem exists_balanced_clipping_parameters
+    (n r : ℕ) (hn : 1 < n) (hr : IsNatCeilSqrt (3 * n) r) :
+    ∃ a b c d : ℕ,
+      0 < a ∧ 0 < b ∧ 0 < c ∧
+      a ≤ b ∧ b ≤ c ∧
+      a + b + c = r ∧
+      a * b + b * c + c * a = n + d ∧
+      d ≤ a + b - 1 := by
+  have hr3 : 3 ≤ r := by
+    by_contra h
+    have hr2 : r ≤ 2 := by omega
+    have hsquare : r ^ 2 ≤ 4 := by nlinarith
+    have : 6 ≤ 3 * n := by omega
+    omega
+  let a := balancedA r
+  let b := balancedB r
+  let c := balancedC r
+  let M := r ^ 2 / 3
+  have hM : a * b + b * c + c * a = M := by
+    simpa [a, b, c, M] using balanced_pair_sum r
+  have hnM : n ≤ M := by
+    dsimp [M]
+    omega
+  let d := M - n
+  refine ⟨a, b, c, d, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · exact (balanced_positive r hr3).1
+  · exact (balanced_positive r hr3).2.1
+  · exact (balanced_positive r hr3).2.2
+  · exact (balanced_order r).1
+  · exact (balanced_order r).2
+  · simpa [a, b, c] using balanced_sum r
+  · dsimp [d]
+    rw [hM]
+    omega
+  · have hlower : (r - 1) ^ 2 / 3 < n := by omega
+    have hwidth := balanced_corner_width r hr3
+    dsimp [d, M, a, b]
+    omega
+
+end OeisA263135
diff --git a/Scratch/A263135PatchCard.lean b/Scratch/A263135PatchCard.lean
new file mode 100644
index 0000000000..4f382b3093
--- /dev/null
+++ b/Scratch/A263135PatchCard.lean
@@ -0,0 +1,82 @@
+import Scratch.A263135PatchCorners
+
+namespace OeisA263135
+
+/-- Raw boxed triples surviving the central diagonal-row interval. -/
+def patchTriples (a b c : ℕ) : Finset ((ℕ × ℕ) × Bool) :=
+  (rankBox (a + b) (b + c)).filter fun x =>
+    b ≤ rankLevel (tripleRankPoint x) ∧
+      rankLevel (tripleRankPoint x) < b + (a + c)
+
+private theorem rankPatch_eq_image_patchTriples (a b c : ℕ) :
+    rankPatch a b c = (patchTriples a b c).image tripleRankPoint := by
+  rfl
+
+private theorem card_rankBox (A B : ℕ) :
+    (rankBox A B).card = 2 * A * B := by
+  simp [rankBox, mul_assoc, mul_left_comm, mul_comm]
+
+private theorem lower_middle_disjoint (a b c : ℕ) :
+    Disjoint
+      ((rankBox (a + b) (b + c)).filter fun x => rankLevel (tripleRankPoint x) < b)
+      (patchTriples a b c) := by
+  rw [Finset.disjoint_left]
+  intro x hl hm
+  exact (not_lt_of_ge (Finset.mem_filter.mp hm).2.1) (Finset.mem_filter.mp hl).2
+
+private theorem lower_union_middle (a b c : ℕ) :
+    ((rankBox (a + b) (b + c)).filter fun x => rankLevel (tripleRankPoint x) < b) ∪
+        patchTriples a b c =
+      (rankBox (a + b) (b + c)).filter fun x =>
+        rankLevel (tripleRankPoint x) < b + (a + c) := by
+  ext x
+  simp [patchTriples]
+  omega
+
+private theorem below_upper_disjoint (a b c : ℕ) :
+    Disjoint
+      ((rankBox (a + b) (b + c)).filter fun x =>
+        rankLevel (tripleRankPoint x) < b + (a + c))
+      (upperCornerTriples (a + b) (b + c) b (a + c)) := by
+  rw [Finset.disjoint_left]
+  intro x hlo hup
+  exact (not_lt_of_ge (Finset.mem_filter.mp hup).2) (Finset.mem_filter.mp hlo).2
+
+private theorem below_union_upper (a b c : ℕ) :
+    ((rankBox (a + b) (b + c)).filter fun x =>
+        rankLevel (tripleRankPoint x) < b + (a + c)) ∪
+      upperCornerTriples (a + b) (b + c) b (a + c) =
+        rankBox (a + b) (b + c) := by
+  ext x
+  simp [upperCornerTriples]
+  omega
+
+/-- Cardinality of the convex ranked patch. -/
+theorem card_rankPatch (a b c : ℕ) :
+    (rankPatch a b c).card = 2 * (a * b + b * c + c * a) := by
+  rw [rankPatch_eq_image_patchTriples,
+    Finset.card_image_of_injective _ tripleRankPoint_injective]
+  have hlower :
+      ((rankBox (a + b) (b + c)).filter fun x =>
+        rankLevel (tripleRankPoint x) < b).card = b ^ 2 := by
+    rw [← lowerCornerTriples_eq_filter_rankBox (a + b) (b + c) b (by omega) (by omega)]
+    exact card_lowerCornerTriples b
+  have hupper :
+      (upperCornerTriples (a + b) (b + c) b (a + c)).card = b ^ 2 := by
+    apply card_upperCornerTriples
+    · ring
+    · omega
+    · omega
+  have hlowmid := congrArg Finset.card (lower_union_middle a b c)
+  rw [Finset.card_union_of_disjoint (lower_middle_disjoint a b c)] at hlowmid
+  have htotal := congrArg Finset.card (below_union_upper a b c)
+  rw [Finset.card_union_of_disjoint (below_upper_disjoint a b c)] at htotal
+  rw [card_rankBox] at htotal
+  nlinarith
+
+/-- Cardinality of the concrete honeycomb patch. -/
+theorem card_patch_formula (a b c : ℕ) :
+    (patch a b c).card = 2 * (a * b + b * c + c * a) := by
+  rw [card_patch, card_rankPatch]
+
+end OeisA263135
diff --git a/Scratch/A263135PatchContacts.lean b/Scratch/A263135PatchContacts.lean
new file mode 100644
index 0000000000..d22e23faef
--- /dev/null
+++ b/Scratch/A263135PatchContacts.lean
@@ -0,0 +1,295 @@
+import Scratch.A263135PatchStructure
+
+namespace OeisA263135
+
+/-- B-side ranked point reached from an A point in the same direction. -/
+def sameRankNeighbor (p : RankPoint) : RankPoint := ⟨p.first, p.second, true⟩
+
+/-- B-side ranked point reached horizontally, when `p.first > 0`. -/
+def horizontalRankNeighbor (p : RankPoint) : RankPoint :=
+  ⟨p.first - 1, p.second, true⟩
+
+/-- B-side ranked point reached diagonally, when `p.second > 0`. -/
+def diagonalRankNeighbor (p : RankPoint) : RankPoint :=
+  ⟨p.first, p.second - 1, true⟩
+
+@[simp]
+theorem neighbor_rankPointVertex_same {p : RankPoint} (hside : p.side = false) :
+    neighbor (rankPointVertex p) .same = rankPointVertex (sameRankNeighbor p) := by
+  rcases p with ⟨i, j, side⟩
+  simp [rankPointVertex, sameRankNeighbor, neighbor] at hside ⊢
+  subst side
+  rfl
+
+@[simp]
+theorem neighbor_rankPointVertex_horizontal {p : RankPoint}
+    (hside : p.side = false) (hi : 0 < p.first) :
+    neighbor (rankPointVertex p) .horizontal = rankPointVertex (horizontalRankNeighbor p) := by
+  rcases p with ⟨i, j, side⟩
+  simp [rankPointVertex, horizontalRankNeighbor, neighbor] at hside hi ⊢
+  subst side
+  apply Vertex.ext <;> simp <;> omega
+
+@[simp]
+theorem neighbor_rankPointVertex_diagonal {p : RankPoint}
+    (hside : p.side = false) (hj : 0 < p.second) :
+    neighbor (rankPointVertex p) .diagonal = rankPointVertex (diagonalRankNeighbor p) := by
+  rcases p with ⟨i, j, side⟩
+  simp [rankPointVertex, diagonalRankNeighbor, neighbor] at hside hj ⊢
+  subst side
+  apply Vertex.ext <;> simp <;> omega
+
+private theorem same_neighbor_mem_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {p : RankPoint} (hp : p ∈ aRankPatch a b c) :
+    neighbor (rankPointVertex p) .same ∈ patch a b c ↔
+      rankLevel p ≠ a + b + c - 1 := by
+  have hpatch := (Finset.mem_filter.mp hp).1
+  have hside := (Finset.mem_filter.mp hp).2
+  rw [neighbor_rankPointVertex_same hside, rankPointVertex_mem_patch_iff, mem_rankPatch]
+  rw [mem_rankPatch] at hpatch
+  rcases p with ⟨i, j, side⟩
+  simp [sameRankNeighbor, rankLevel] at hside hpatch ⊢
+  subst side
+  omega
+
+private theorem horizontal_neighbor_mem_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {p : RankPoint} (hp : p ∈ aRankPatch a b c) :
+    neighbor (rankPointVertex p) .horizontal ∈ patch a b c ↔ p.first ≠ 0 := by
+  have hpatch := (Finset.mem_filter.mp hp).1
+  have hside := (Finset.mem_filter.mp hp).2
+  constructor
+  · intro hn hzero
+    rcases Finset.mem_image.mp hn with ⟨q, hq, heq⟩
+    have hi := congrArg Vertex.i heq
+    rcases p with ⟨i, j, side⟩
+    rcases q with ⟨k, l, side'⟩
+    simp [rankPointVertex, neighbor] at hside hzero hi
+    subst side
+    omega
+  · intro hzero
+    have hi : 0 < p.first := Nat.pos_of_ne_zero hzero
+    rw [neighbor_rankPointVertex_horizontal hside hi, rankPointVertex_mem_patch_iff,
+      mem_rankPatch]
+    rw [mem_rankPatch] at hpatch
+    rcases p with ⟨i, j, side⟩
+    simp [horizontalRankNeighbor, rankLevel] at hside hpatch ⊢
+    subst side
+    omega
+
+private theorem diagonal_neighbor_mem_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {p : RankPoint} (hp : p ∈ aRankPatch a b c) :
+    neighbor (rankPointVertex p) .diagonal ∈ patch a b c ↔ p.second ≠ 0 := by
+  have hpatch := (Finset.mem_filter.mp hp).1
+  have hside := (Finset.mem_filter.mp hp).2
+  constructor
+  · intro hn hzero
+    rcases Finset.mem_image.mp hn with ⟨q, hq, heq⟩
+    have hj := congrArg Vertex.j heq
+    rcases p with ⟨i, j, side⟩
+    rcases q with ⟨k, l, side'⟩
+    simp [rankPointVertex, neighbor] at hside hzero hj
+    subst side
+    omega
+  · intro hzero
+    have hj : 0 < p.second := Nat.pos_of_ne_zero hzero
+    rw [neighbor_rankPointVertex_diagonal hside hj, rankPointVertex_mem_patch_iff,
+      mem_rankPatch]
+    rw [mem_rankPatch] at hpatch
+    rcases p with ⟨i, j, side⟩
+    simp [diagonalRankNeighbor, rankLevel] at hside hpatch ⊢
+    subst side
+    omega
+
+/-- A points contributing a same-direction internal dart. -/
+def sameContactPoints (a b c : ℕ) : Finset RankPoint :=
+  (aRankPatch a b c).filter fun p => rankLevel p ≠ a + b + c - 1
+
+/-- A points contributing a horizontal internal dart. -/
+def horizontalContactPoints (a b c : ℕ) : Finset RankPoint :=
+  (aRankPatch a b c).filter fun p => p.first ≠ 0
+
+/-- A points contributing a diagonal internal dart. -/
+def diagonalContactPoints (a b c : ℕ) : Finset RankPoint :=
+  (aRankPatch a b c).filter fun p => p.second ≠ 0
+
+private theorem card_complementary_filter
+    {α : Type*} [DecidableEq α] (S : Finset α) (P : α → Prop) [DecidablePred P] :
+    (S.filter fun x => ¬ P x).card + (S.filter P).card = S.card := by
+  have hu : (S.filter fun x => ¬ P x) ∪ S.filter P = S := by
+    ext x
+    by_cases h : P x <;> simp [h]
+  have hd : Disjoint (S.filter fun x => ¬ P x) (S.filter P) := by
+    rw [Finset.disjoint_left]
+    simp
+  simpa [Finset.card_union_of_disjoint hd] using congrArg Finset.card hu
+
+private theorem card_sameContactPoints (a b c : ℕ)
+    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (sameContactPoints a b c).card = a * b + b * c + c * a - b := by
+  have h := card_complementary_filter (aRankPatch a b c)
+    (fun p => rankLevel p = a + b + c - 1)
+  rw [← topARankPatch, card_topARankPatch a b c ha hb hc, card_aRankPatch] at h
+  simpa [sameContactPoints] using (show
+    (sameContactPoints a b c).card + b = a * b + b * c + c * a by simpa using h)
+
+private theorem card_horizontalContactPoints (a b c : ℕ)
+    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (horizontalContactPoints a b c).card = a * b + b * c + c * a - c := by
+  have h := card_complementary_filter (aRankPatch a b c) (fun p => p.first = 0)
+  rw [← firstZeroARankPatch, card_firstZeroARankPatch a b c ha hb hc,
+    card_aRankPatch] at h
+  simpa [horizontalContactPoints] using (show
+    (horizontalContactPoints a b c).card + c = a * b + b * c + c * a by simpa using h)
+
+private theorem card_diagonalContactPoints (a b c : ℕ)
+    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (diagonalContactPoints a b c).card = a * b + b * c + c * a - a := by
+  have h := card_complementary_filter (aRankPatch a b c) (fun p => p.second = 0)
+  rw [← secondZeroARankPatch, card_secondZeroARankPatch a b c ha hb hc,
+    card_aRankPatch] at h
+  simpa [diagonalContactPoints] using (show
+    (diagonalContactPoints a b c).card + a = a * b + b * c + c * a by simpa using h)
+
+/-- Ranked representatives of all A-based internal darts of the convex patch. -/
+def patchContactDarts (a b c : ℕ) : Finset (RankPoint × Direction) :=
+  (sameContactPoints a b c ×ˢ {.same}) ∪
+    (horizontalContactPoints a b c ×ˢ {.horizontal}) ∪
+      (diagonalContactPoints a b c ×ˢ {.diagonal})
+
+private theorem patchContactDarts_pairwise_disjoint (a b c : ℕ) :
+    Disjoint (sameContactPoints a b c ×ˢ {.same})
+      (horizontalContactPoints a b c ×ˢ {.horizontal}) ∧
+    Disjoint ((sameContactPoints a b c ×ˢ {.same}) ∪
+      (horizontalContactPoints a b c ×ˢ {.horizontal}))
+      (diagonalContactPoints a b c ×ˢ {.diagonal}) := by
+  constructor <;> rw [Finset.disjoint_left] <;> simp
+
+private theorem card_patchContactDarts (a b c : ℕ)
+    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (patchContactDarts a b c).card =
+      3 * (a * b + b * c + c * a) - (a + b + c) := by
+  rcases patchContactDarts_pairwise_disjoint a b c with ⟨h12, h123⟩
+  rw [patchContactDarts, Finset.card_union_of_disjoint h123,
+    Finset.card_union_of_disjoint h12]
+  simp only [Finset.card_product, Finset.card_singleton, mul_one,
+    card_sameContactPoints a b c ha hb hc,
+    card_horizontalContactPoints a b c ha hb hc,
+    card_diagonalContactPoints a b c ha hb hc]
+  have haM : a ≤ a * b + b * c + c * a := by nlinarith
+  have hbM : b ≤ a * b + b * c + c * a := by nlinarith
+  have hcM : c ≤ a * b + b * c + c * a := by nlinarith
+  omega
+
+private def rankDartVertex (pd : RankPoint × Direction) : Vertex × Direction :=
+  (rankPointVertex pd.1, pd.2)
+
+private theorem rankDartVertex_injective : Function.Injective rankDartVertex := by
+  intro p q h
+  apply Prod.ext
+  · exact rankPointVertex_injective (congrArg Prod.fst h)
+  · exact congrArg Prod.snd h
+
+private theorem rankDart_mem_aInternal_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {pd : RankPoint × Direction} :
+    pd ∈ patchContactDarts a b c ↔
+      rankDartVertex pd ∈ aInternalDarts (patch a b c) := by
+  rcases pd with ⟨p, d⟩
+  cases d with
+  | same =>
+      constructor
+      · intro hpd
+        have hp : p ∈ sameContactPoints a b c := by
+          simpa [patchContactDarts] using hpd
+        have hpA := (Finset.mem_filter.mp hp).1
+        have hnot := (Finset.mem_filter.mp hp).2
+        apply Finset.mem_filter.mpr
+        refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+          ⟨rankPointVertex_mem_patch_iff.mpr (Finset.mem_filter.mp hpA).1,
+            Finset.mem_univ _⟩, ?_⟩, ?_⟩
+        · exact (same_neighbor_mem_iff ha hb hc hpA).mpr hnot
+        · simpa [rankDartVertex, rankPointVertex] using
+            (Finset.mem_filter.mp hpA).2
+      · intro hint
+        rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+        rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+        have hpPatch := rankPointVertex_mem_patch_iff.mp
+          (Finset.mem_product.mp hprod).1
+        have hpA : p ∈ aRankPatch a b c := Finset.mem_filter.mpr
+          ⟨hpPatch, by simpa [rankDartVertex, rankPointVertex] using hside⟩
+        have hp : p ∈ sameContactPoints a b c := Finset.mem_filter.mpr
+          ⟨hpA, (same_neighbor_mem_iff ha hb hc hpA).mp hn⟩
+        simpa [patchContactDarts] using hp
+  | horizontal =>
+      constructor
+      · intro hpd
+        have hp : p ∈ horizontalContactPoints a b c := by
+          simpa [patchContactDarts] using hpd
+        have hpA := (Finset.mem_filter.mp hp).1
+        have hnot := (Finset.mem_filter.mp hp).2
+        apply Finset.mem_filter.mpr
+        refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+          ⟨rankPointVertex_mem_patch_iff.mpr (Finset.mem_filter.mp hpA).1,
+            Finset.mem_univ _⟩,
+          (horizontal_neighbor_mem_iff ha hb hc hpA).mpr hnot⟩, ?_⟩
+        simpa [rankDartVertex, rankPointVertex] using
+          (Finset.mem_filter.mp hpA).2
+      · intro hint
+        rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+        rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+        have hpPatch := rankPointVertex_mem_patch_iff.mp
+          (Finset.mem_product.mp hprod).1
+        have hpA : p ∈ aRankPatch a b c := Finset.mem_filter.mpr
+          ⟨hpPatch, by simpa [rankDartVertex, rankPointVertex] using hside⟩
+        have hp : p ∈ horizontalContactPoints a b c := Finset.mem_filter.mpr
+          ⟨hpA, (horizontal_neighbor_mem_iff ha hb hc hpA).mp hn⟩
+        simpa [patchContactDarts] using hp
+  | diagonal =>
+      constructor
+      · intro hpd
+        have hp : p ∈ diagonalContactPoints a b c := by
+          simpa [patchContactDarts] using hpd
+        have hpA := (Finset.mem_filter.mp hp).1
+        have hnot := (Finset.mem_filter.mp hp).2
+        apply Finset.mem_filter.mpr
+        refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+          ⟨rankPointVertex_mem_patch_iff.mpr (Finset.mem_filter.mp hpA).1,
+            Finset.mem_univ _⟩,
+          (diagonal_neighbor_mem_iff ha hb hc hpA).mpr hnot⟩, ?_⟩
+        simpa [rankDartVertex, rankPointVertex] using
+          (Finset.mem_filter.mp hpA).2
+      · intro hint
+        rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+        rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+        have hpPatch := rankPointVertex_mem_patch_iff.mp
+          (Finset.mem_product.mp hprod).1
+        have hpA : p ∈ aRankPatch a b c := Finset.mem_filter.mpr
+          ⟨hpPatch, by simpa [rankDartVertex, rankPointVertex] using hside⟩
+        have hp : p ∈ diagonalContactPoints a b c := Finset.mem_filter.mpr
+          ⟨hpA, (diagonal_neighbor_mem_iff ha hb hc hpA).mp hn⟩
+        simpa [patchContactDarts] using hp
+
+/-- Exact contact count of a convex patch. -/
+theorem contacts_patch_formula (a b c : ℕ)
+    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    contacts (patch a b c) =
+      3 * (a * b + b * c + c * a) - (a + b + c) := by
+  rw [contacts_eq_card_aInternalDarts]
+  rw [← card_patchContactDarts a b c ha hb hc]
+  symm
+  apply Finset.card_bij (fun pd hpd => rankDartVertex pd)
+  · exact fun pd hpd => (rankDart_mem_aInternal_iff ha hb hc).mp hpd
+  · intro p hp q hq h
+    exact rankDartVertex_injective h
+  · intro vd hvd
+    rcases vd with ⟨v, d⟩
+    rcases Finset.mem_filter.mp hvd with ⟨hint, hside⟩
+    rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+    rcases Finset.mem_image.mp (Finset.mem_product.mp hprod).1 with ⟨p, hp, rfl⟩
+    refine ⟨(p, d), (rankDart_mem_aInternal_iff ha hb hc).mpr ?_, rfl⟩
+    exact Finset.mem_filter.mpr ⟨hint, hside⟩
+
+end OeisA263135
diff --git a/Scratch/A263135PatchCorners.lean b/Scratch/A263135PatchCorners.lean
new file mode 100644
index 0000000000..0518b9775e
--- /dev/null
+++ b/Scratch/A263135PatchCorners.lean
@@ -0,0 +1,133 @@
+import Scratch.A263135PatchDefs
+
+namespace OeisA263135
+
+/-- Natural-coordinate pairs strictly below diagonal level `b`. -/
+def lowerPairs (b : ℕ) : Finset (ℕ × ℕ) :=
+  (Finset.range b).biUnion Finset.Nat.antidiagonal
+
+@[simp]
+theorem mem_lowerPairs {b i j : ℕ} :
+    (i, j) ∈ lowerPairs b ↔ i + j < b := by
+  constructor
+  · intro h
+    rcases Finset.mem_biUnion.mp h with ⟨n, hn, hij⟩
+    have hs := Finset.mem_antidiagonal.mp hij
+    omega
+  · intro h
+    apply Finset.mem_biUnion.mpr
+    exact ⟨i + j, Finset.mem_range.mpr h, Finset.mem_antidiagonal.mpr rfl⟩
+
+private theorem antidiagonal_pairwise_disjoint (b : ℕ) :
+    (Finset.range b).toSet.PairwiseDisjoint Finset.Nat.antidiagonal := by
+  intro m hm n hn hmn
+  rw [Finset.disjoint_left]
+  intro p hpm hpn
+  have hm' := Finset.mem_antidiagonal.mp hpm
+  have hn' := Finset.mem_antidiagonal.mp hpn
+  exact hmn (hm'.symm.trans hn')
+
+/-- Cardinality of the strict lower triangle as a sum of antidiagonal sizes. -/
+theorem card_lowerPairs (b : ℕ) :
+    (lowerPairs b).card = ∑ n ∈ Finset.range b, (n + 1) := by
+  rw [lowerPairs, Finset.card_biUnion]
+  · simp
+  · exact antidiagonal_pairwise_disjoint b
+
+/-- Lower excluded corner of a rank box, split by honeycomb side. -/
+def lowerCornerTriples (b : ℕ) : Finset ((ℕ × ℕ) × Bool) :=
+  (lowerPairs b ×ˢ {false}) ∪ (lowerPairs (b - 1) ×ˢ {true})
+
+private theorem lower_corner_sides_disjoint (b : ℕ) :
+    Disjoint (lowerPairs b ×ˢ {false}) (lowerPairs (b - 1) ×ˢ {true}) := by
+  rw [Finset.disjoint_left]
+  intro x hx hy
+  have hf := (Finset.mem_product.mp hx).2
+  have ht := (Finset.mem_product.mp hy).2
+  simp at hf ht
+
+/-- The lower excluded corner contains exactly `b²` ranked points. -/
+theorem card_lowerCornerTriples (b : ℕ) :
+    (lowerCornerTriples b).card = b ^ 2 := by
+  rw [lowerCornerTriples,
+    Finset.card_union_of_disjoint (lower_corner_sides_disjoint b)]
+  simp only [Finset.card_product, Finset.card_singleton, mul_one,
+    card_lowerPairs]
+  by_cases hb : b = 0
+  · subst b
+    simp
+  · have hb1 : 1 ≤ b := Nat.one_le_iff_ne_zero.mpr hb
+    have hgauss1 := Finset.sum_range_id_mul_two b
+    have hgauss2 := Finset.sum_range_id_mul_two (b - 1)
+    simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range,
+      Nat.nsmul_eq_mul, mul_one] at *
+    nlinarith
+
+/-- The lower-corner description agrees with filtering any sufficiently large box by level. -/
+theorem lowerCornerTriples_eq_filter_rankBox
+    (A B b : ℕ) (hbA : b ≤ A) (hbB : b ≤ B) :
+    lowerCornerTriples b =
+      (rankBox A B).filter fun x => rankLevel (tripleRankPoint x) < b := by
+  ext x
+  rcases x with ⟨⟨i, j⟩, side⟩
+  cases side <;>
+    simp [lowerCornerTriples, rankBox, rankLevel, tripleRankPoint, mem_lowerPairs] <;>
+    omega
+
+/-- Central reflection of a finite rank box. -/
+def reflectTriple (A B : ℕ) (x : (ℕ × ℕ) × Bool) : (ℕ × ℕ) × Bool :=
+  ((A - 1 - x.1.1, B - 1 - x.1.2), !x.2)
+
+private theorem reflectTriple_involutive_on_box
+    {A B : ℕ} {x : (ℕ × ℕ) × Bool} (hx : x ∈ rankBox A B) :
+    reflectTriple A B (reflectTriple A B x) = x := by
+  rcases x with ⟨⟨i, j⟩, side⟩
+  simp [rankBox] at hx
+  rcases hx with ⟨hi, hj⟩
+  apply Prod.ext
+  · apply Prod.ext <;> simp [reflectTriple] <;> omega
+  · simp [reflectTriple]
+
+private theorem reflectTriple_mem_box
+    {A B : ℕ} {x : (ℕ × ℕ) × Bool} (hx : x ∈ rankBox A B) :
+    reflectTriple A B x ∈ rankBox A B := by
+  rcases x with ⟨⟨i, j⟩, side⟩
+  simp [rankBox] at hx ⊢
+  omega
+
+/-- Upper excluded corner of the patch interval. -/
+def upperCornerTriples (A B b C : ℕ) : Finset ((ℕ × ℕ) × Bool) :=
+  (rankBox A B).filter fun x => b + C ≤ rankLevel (tripleRankPoint x)
+
+/-- Reflection maps the upper corner bijectively to the lower corner when `A+B=C+2b`. -/
+theorem card_upperCornerTriples
+    (A B b C : ℕ) (hsum : A + B = C + 2 * b) (hbA : b ≤ A) (hbB : b ≤ B) :
+    (upperCornerTriples A B b C).card = b ^ 2 := by
+  have htarget := lowerCornerTriples_eq_filter_rankBox A B b hbA hbB
+  rw [← htarget, ← card_lowerCornerTriples b]
+  apply Finset.card_bij (fun x hx => reflectTriple A B x)
+  · intro x hx
+    have hxbox := (Finset.mem_filter.mp hx).1
+    have hxupper := (Finset.mem_filter.mp hx).2
+    rw [lowerCornerTriples_eq_filter_rankBox A B b hbA hbB]
+    apply Finset.mem_filter.mpr
+    refine ⟨reflectTriple_mem_box hxbox, ?_⟩
+    rcases x with ⟨⟨i, j⟩, side⟩
+    cases side <;> simp [reflectTriple, rankLevel, tripleRankPoint] at hxbox hxupper ⊢ <;> omega
+  · intro x hx y hy hxy
+    have hxbox := (Finset.mem_filter.mp hx).1
+    have hybox := (Finset.mem_filter.mp hy).1
+    rw [← reflectTriple_involutive_on_box hxbox,
+      ← reflectTriple_involutive_on_box hybox, hxy]
+  · intro y hy
+    rw [lowerCornerTriples_eq_filter_rankBox A B b hbA hbB] at hy
+    have hybox := (Finset.mem_filter.mp hy).1
+    refine ⟨reflectTriple A B y, ?_, ?_⟩
+    · apply Finset.mem_filter.mpr
+      refine ⟨reflectTriple_mem_box hybox, ?_⟩
+      have hylower := (Finset.mem_filter.mp hy).2
+      rcases y with ⟨⟨i, j⟩, side⟩
+      cases side <;> simp [reflectTriple, rankLevel, tripleRankPoint] at hybox hylower ⊢ <;> omega
+    · exact reflectTriple_involutive_on_box hybox
+
+end OeisA263135
diff --git a/Scratch/A263135PatchDefs.lean b/Scratch/A263135PatchDefs.lean
new file mode 100644
index 0000000000..b3de642bd8
--- /dev/null
+++ b/Scratch/A263135PatchDefs.lean
@@ -0,0 +1,81 @@
+import Scratch.A263135Parameters
+
+namespace OeisA263135
+
+/-- Finite coordinate box used for the convex honeycomb patch. -/
+def rankBox (A B : ℕ) : Finset ((ℕ × ℕ) × Bool) :=
+  (Finset.range A ×ˢ Finset.range B) ×ˢ Finset.univ
+
+/-- Convert a boxed coordinate triple into a ranked honeycomb point. -/
+def tripleRankPoint (x : (ℕ × ℕ) × Bool) : RankPoint :=
+  ⟨x.1.1, x.1.2, x.2⟩
+
+theorem tripleRankPoint_injective : Function.Injective tripleRankPoint := by
+  rintro ⟨⟨i, j⟩, s⟩ ⟨⟨k, l⟩, t⟩ h
+  simp [tripleRankPoint] at h ⊢
+  exact h
+
+/-- Integer level of a ranked honeycomb point in the diagonal row direction. -/
+def rankLevel (p : RankPoint) : ℕ := p.first + p.second + if p.side then 1 else 0
+
+/-- Convex patch with alternating side parameters `a,b,c,a,b,c`, in ranked coordinates. -/
+def rankPatch (a b c : ℕ) : Finset RankPoint :=
+  ((rankBox (a + b) (b + c)).filter fun x =>
+      b ≤ rankLevel (tripleRankPoint x) ∧
+        rankLevel (tripleRankPoint x) < b + (a + c)).image tripleRankPoint
+
+/-- Convert ranked coordinates to the honeycomb coordinates used by `Vertex`. -/
+def rankPointVertex (p : RankPoint) : Vertex :=
+  ⟨p.first, (p.second : ℤ) - 1, p.side⟩
+
+theorem rankPointVertex_injective : Function.Injective rankPointVertex := by
+  intro p q h
+  apply RankPoint.ext
+  · have hi := congrArg Vertex.i h
+    exact_mod_cast hi
+  · have hj := congrArg Vertex.j h
+    omega
+  · exact congrArg Vertex.side h
+
+/-- The concrete finite honeycomb patch. -/
+def patch (a b c : ℕ) : Finset Vertex :=
+  (rankPatch a b c).image rankPointVertex
+
+@[simp]
+theorem card_patch (a b c : ℕ) :
+    (patch a b c).card = (rankPatch a b c).card := by
+  exact Finset.card_image_of_injective _ rankPointVertex_injective
+
+@[simp]
+theorem rowCoord_rankPointVertex_first (p : RankPoint) :
+    rowCoord .first (rankPointVertex p) = p.first := by
+  simp [rankPointVertex, rowCoord]
+
+@[simp]
+theorem rowCoord_rankPointVertex_second (p : RankPoint) :
+    rowCoord .second (rankPointVertex p) = (p.second : ℤ) - 1 := by
+  simp [rankPointVertex, rowCoord]
+
+@[simp]
+theorem rowCoord_rankPointVertex_diagonal (p : RankPoint) :
+    rowCoord .diagonal (rankPointVertex p) = (rankLevel p : ℤ) - 1 := by
+  rcases p with ⟨i, j, side⟩
+  cases side <;> simp [rankPointVertex, rowCoord, rankLevel] <;> omega
+
+/-- Lower clipped corner pair, in ranked coordinates. -/
+def clipPair (a b : ℕ) (k : ℕ) : Finset RankPoint :=
+  if k < b then
+    {⟨k, b - 1 - k, true⟩, ⟨k, b - k, false⟩}
+  else
+    let h := k - b
+    {⟨h, b - h, true⟩, ⟨h, b + 1 - h, false⟩}
+
+/-- All pairs removed in the first `d` corner-clipping steps. -/
+def clippedRankPoints (a b d : ℕ) : Finset RankPoint :=
+  (Finset.range d).biUnion fun k => clipPair a b k
+
+/-- Patch after `d` successive corner-pair removals. -/
+def clippedPatch (a b c d : ℕ) : Finset Vertex :=
+  ((rankPatch a b c) \ clippedRankPoints a b d).image rankPointVertex
+
+end OeisA263135
diff --git a/Scratch/A263135PatchStructure.lean b/Scratch/A263135PatchStructure.lean
new file mode 100644
index 0000000000..9fef55a67d
--- /dev/null
+++ b/Scratch/A263135PatchStructure.lean
@@ -0,0 +1,190 @@
+import Scratch.A263135PatchCard
+
+namespace OeisA263135
+
+@[simp]
+theorem mem_rankPatch {a b c : ℕ} {p : RankPoint} :
+    p ∈ rankPatch a b c ↔
+      p.first < a + b ∧ p.second < b + c ∧
+        b ≤ rankLevel p ∧ rankLevel p < b + (a + c) := by
+  constructor
+  · intro hp
+    rcases Finset.mem_image.mp hp with ⟨x, hx, rfl⟩
+    rcases Finset.mem_filter.mp hx with ⟨hbox, hlev⟩
+    rcases x with ⟨⟨i, j⟩, side⟩
+    simpa [rankBox, tripleRankPoint] using And.intro hbox hlev
+  · rintro ⟨hi, hj, hlo, hhi⟩
+    let x : (ℕ × ℕ) × Bool := ((p.first, p.second), p.side)
+    apply Finset.mem_image.mpr
+    refine ⟨x, ?_, ?_⟩
+    · apply Finset.mem_filter.mpr
+      exact ⟨by simp [rankBox, x, hi, hj], by simpa [x, tripleRankPoint]⟩
+    · rcases p with ⟨i, j, side⟩
+      rfl
+
+@[simp]
+theorem rankPointVertex_mem_patch_iff {a b c : ℕ} {p : RankPoint} :
+    rankPointVertex p ∈ patch a b c ↔ p ∈ rankPatch a b c := by
+  constructor
+  · intro h
+    rcases Finset.mem_image.mp h with ⟨q, hq, heq⟩
+    exact rankPointVertex_injective heq ▸ hq
+  · exact fun h => Finset.mem_image.mpr ⟨p, h, rfl⟩
+
+/-- A-side ranked vertices in a patch. -/
+def aRankPatch (a b c : ℕ) : Finset RankPoint :=
+  (rankPatch a b c).filter fun p => p.side = false
+
+/-- B-side ranked vertices in a patch. -/
+def bRankPatch (a b c : ℕ) : Finset RankPoint :=
+  (rankPatch a b c).filter fun p => p.side = true
+
+private theorem a_b_rankPatch_disjoint (a b c : ℕ) :
+    Disjoint (aRankPatch a b c) (bRankPatch a b c) := by
+  rw [Finset.disjoint_left]
+  intro p ha hb
+  have hf := (Finset.mem_filter.mp ha).2
+  have ht := (Finset.mem_filter.mp hb).2
+  simp [hf] at ht
+
+private theorem a_union_b_rankPatch (a b c : ℕ) :
+    aRankPatch a b c ∪ bRankPatch a b c = rankPatch a b c := by
+  ext p
+  simp [aRankPatch, bRankPatch]
+  cases h : p.side <;> simp [h]
+
+/-- Central reflection of ranked patch coordinates. -/
+def reflectRankPoint (a b c : ℕ) (p : RankPoint) : RankPoint :=
+  ⟨a + b - 1 - p.first, b + c - 1 - p.second, !p.side⟩
+
+private theorem reflectRankPoint_mem
+    {a b c : ℕ} {p : RankPoint} (hp : p ∈ rankPatch a b c) :
+    reflectRankPoint a b c p ∈ rankPatch a b c := by
+  rw [mem_rankPatch] at hp ⊢
+  rcases p with ⟨i, j, side⟩
+  cases side <;> simp [reflectRankPoint, rankLevel] at hp ⊢ <;> omega
+
+private theorem reflectRankPoint_involutive
+    {a b c : ℕ} {p : RankPoint} (hp : p ∈ rankPatch a b c) :
+    reflectRankPoint a b c (reflectRankPoint a b c p) = p := by
+  rw [mem_rankPatch] at hp
+  rcases p with ⟨i, j, side⟩
+  simp [reflectRankPoint]
+  omega
+
+/-- The two bipartite sides of a convex patch have equal cardinality. -/
+theorem card_aRankPatch_eq_card_bRankPatch (a b c : ℕ) :
+    (aRankPatch a b c).card = (bRankPatch a b c).card := by
+  apply Finset.card_bij (fun p hp => reflectRankPoint a b c p)
+  · intro p hp
+    apply Finset.mem_filter.mpr
+    refine ⟨reflectRankPoint_mem (Finset.mem_filter.mp hp).1, ?_⟩
+    simpa [reflectRankPoint, (Finset.mem_filter.mp hp).2]
+  · intro p hp q hq h
+    rw [← reflectRankPoint_involutive (Finset.mem_filter.mp hp).1,
+      ← reflectRankPoint_involutive (Finset.mem_filter.mp hq).1, h]
+  · intro q hq
+    refine ⟨reflectRankPoint a b c q, ?_, ?_⟩
+    · apply Finset.mem_filter.mpr
+      refine ⟨reflectRankPoint_mem (Finset.mem_filter.mp hq).1, ?_⟩
+      simpa [reflectRankPoint, (Finset.mem_filter.mp hq).2]
+    · exact reflectRankPoint_involutive (Finset.mem_filter.mp hq).1
+
+/-- Each bipartite side has `ab+bc+ca` vertices. -/
+theorem card_aRankPatch (a b c : ℕ) :
+    (aRankPatch a b c).card = a * b + b * c + c * a := by
+  have htotal := congrArg Finset.card (a_union_b_rankPatch a b c)
+  rw [Finset.card_union_of_disjoint (a_b_rankPatch_disjoint a b c),
+    card_rankPatch, card_aRankPatch_eq_card_bRankPatch] at htotal
+  omega
+
+/-- A-side vertices on the top diagonal row. -/
+def topARankPatch (a b c : ℕ) : Finset RankPoint :=
+  (aRankPatch a b c).filter fun p => rankLevel p = a + b + c - 1
+
+/-- A-side vertices on the first-coordinate boundary. -/
+def firstZeroARankPatch (a b c : ℕ) : Finset RankPoint :=
+  (aRankPatch a b c).filter fun p => p.first = 0
+
+/-- A-side vertices on the second-coordinate boundary. -/
+def secondZeroARankPatch (a b c : ℕ) : Finset RankPoint :=
+  (aRankPatch a b c).filter fun p => p.second = 0
+
+/-- The top A-side row has length `b`. -/
+theorem card_topARankPatch (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (topARankPatch a b c).card = b := by
+  conv_rhs => rw [← Finset.card_range b]
+  symm
+  apply Finset.card_bij (fun k hk => (⟨a + k, b + c - 1 - k, false⟩ : RankPoint))
+  · intro k hk
+    have hk' := Finset.mem_range.mp hk
+    apply Finset.mem_filter.mpr
+    refine ⟨Finset.mem_filter.mpr ⟨?_, rfl⟩, ?_⟩
+    · rw [mem_rankPatch]
+      simp [rankLevel]
+      omega
+    · simp [rankLevel]
+      omega
+  · intro k hk l hl h
+    have := congrArg RankPoint.first h
+    omega
+  · intro p hp
+    rcases Finset.mem_filter.mp hp with ⟨haP, htop⟩
+    rcases Finset.mem_filter.mp haP with ⟨hpatch, hside⟩
+    rw [mem_rankPatch] at hpatch
+    rcases p with ⟨i, j, side⟩
+    simp [rankLevel] at hside htop hpatch
+    refine ⟨i - a, Finset.mem_range.mpr (by omega), ?_⟩
+    apply RankPoint.ext <;> simp <;> omega
+
+/-- The first-coordinate A-side boundary has length `c`. -/
+theorem card_firstZeroARankPatch (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (firstZeroARankPatch a b c).card = c := by
+  conv_rhs => rw [← Finset.card_range c]
+  symm
+  apply Finset.card_bij (fun k hk => (⟨0, b + k, false⟩ : RankPoint))
+  · intro k hk
+    have hk' := Finset.mem_range.mp hk
+    apply Finset.mem_filter.mpr
+    refine ⟨Finset.mem_filter.mpr ⟨?_, rfl⟩, rfl⟩
+    rw [mem_rankPatch]
+    simp [rankLevel]
+    omega
+  · intro k hk l hl h
+    have := congrArg RankPoint.second h
+    omega
+  · intro p hp
+    rcases Finset.mem_filter.mp hp with ⟨haP, hfirst⟩
+    rcases Finset.mem_filter.mp haP with ⟨hpatch, hside⟩
+    rw [mem_rankPatch] at hpatch
+    rcases p with ⟨i, j, side⟩
+    simp [rankLevel] at hfirst hside hpatch
+    refine ⟨j - b, Finset.mem_range.mpr (by omega), ?_⟩
+    apply RankPoint.ext <;> simp <;> omega
+
+/-- The second-coordinate A-side boundary has length `a`. -/
+theorem card_secondZeroARankPatch (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (secondZeroARankPatch a b c).card = a := by
+  conv_rhs => rw [← Finset.card_range a]
+  symm
+  apply Finset.card_bij (fun k hk => (⟨b + k, 0, false⟩ : RankPoint))
+  · intro k hk
+    have hk' := Finset.mem_range.mp hk
+    apply Finset.mem_filter.mpr
+    refine ⟨Finset.mem_filter.mpr ⟨?_, rfl⟩, rfl⟩
+    rw [mem_rankPatch]
+    simp [rankLevel]
+    omega
+  · intro k hk l hl h
+    have := congrArg RankPoint.first h
+    omega
+  · intro p hp
+    rcases Finset.mem_filter.mp hp with ⟨haP, hsecond⟩
+    rcases Finset.mem_filter.mp haP with ⟨hpatch, hside⟩
+    rw [mem_rankPatch] at hpatch
+    rcases p with ⟨i, j, side⟩
+    simp [rankLevel] at hsecond hside hpatch
+    refine ⟨i - b, Finset.mem_range.mpr (by omega), ?_⟩
+    apply RankPoint.ext <;> simp <;> omega
+
+end OeisA263135
diff --git a/Scratch/A263135RankDarts.lean b/Scratch/A263135RankDarts.lean
new file mode 100644
index 0000000000..f1f392c2c7
--- /dev/null
+++ b/Scratch/A263135RankDarts.lean
@@ -0,0 +1,197 @@
+import Scratch.A263135ClippingGeometry
+
+namespace OeisA263135
+
+/-- Convert a ranked A-based dart to the concrete honeycomb coordinates. -/
+def clippingRankDartVertex (pd : RankPoint × Direction) : Vertex × Direction :=
+  (rankPointVertex pd.1, pd.2)
+
+@[simp]
+theorem clippingRankDartVertex_fst (pd : RankPoint × Direction) :
+    (clippingRankDartVertex pd).1 = rankPointVertex pd.1 := rfl
+
+@[simp]
+theorem clippingRankDartVertex_snd (pd : RankPoint × Direction) :
+    (clippingRankDartVertex pd).2 = pd.2 := rfl
+
+/-- The ranked-dart conversion is injective. -/
+theorem clippingRankDartVertex_injective : Function.Injective clippingRankDartVertex := by
+  intro p q h
+  apply Prod.ext
+  · exact rankPointVertex_injective (congrArg Prod.fst h)
+  · exact congrArg Prod.snd h
+
+private theorem clipping_same_neighbor_mem_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {p : RankPoint} (hp : p ∈ aRankPatch a b c) :
+    neighbor (rankPointVertex p) .same ∈ patch a b c ↔
+      rankLevel p ≠ a + b + c - 1 := by
+  have hpatch := (Finset.mem_filter.mp hp).1
+  have hside := (Finset.mem_filter.mp hp).2
+  rw [neighbor_rankPointVertex_same hside, rankPointVertex_mem_patch_iff, mem_rankPatch]
+  rw [mem_rankPatch] at hpatch
+  rcases p with ⟨i, j, side⟩
+  simp [sameRankNeighbor, rankLevel] at hside hpatch ⊢
+  subst side
+  omega
+
+private theorem clipping_horizontal_neighbor_mem_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {p : RankPoint} (hp : p ∈ aRankPatch a b c) :
+    neighbor (rankPointVertex p) .horizontal ∈ patch a b c ↔ p.first ≠ 0 := by
+  have hpatch := (Finset.mem_filter.mp hp).1
+  have hside := (Finset.mem_filter.mp hp).2
+  constructor
+  · intro hn hzero
+    rcases Finset.mem_image.mp hn with ⟨q, hq, heq⟩
+    have hi := congrArg Vertex.i heq
+    rcases p with ⟨i, j, side⟩
+    rcases q with ⟨k, l, side'⟩
+    simp [rankPointVertex, neighbor] at hside hzero hi
+    subst side
+    omega
+  · intro hzero
+    have hi : 0 < p.first := Nat.pos_of_ne_zero hzero
+    rw [neighbor_rankPointVertex_horizontal hside hi, rankPointVertex_mem_patch_iff,
+      mem_rankPatch]
+    rw [mem_rankPatch] at hpatch
+    rcases p with ⟨i, j, side⟩
+    simp [horizontalRankNeighbor, rankLevel] at hside hpatch ⊢
+    subst side
+    omega
+
+private theorem clipping_diagonal_neighbor_mem_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {p : RankPoint} (hp : p ∈ aRankPatch a b c) :
+    neighbor (rankPointVertex p) .diagonal ∈ patch a b c ↔ p.second ≠ 0 := by
+  have hpatch := (Finset.mem_filter.mp hp).1
+  have hside := (Finset.mem_filter.mp hp).2
+  constructor
+  · intro hn hzero
+    rcases Finset.mem_image.mp hn with ⟨q, hq, heq⟩
+    have hj := congrArg Vertex.j heq
+    rcases p with ⟨i, j, side⟩
+    rcases q with ⟨k, l, side'⟩
+    simp [rankPointVertex, neighbor] at hside hzero hj
+    subst side
+    omega
+  · intro hzero
+    have hj : 0 < p.second := Nat.pos_of_ne_zero hzero
+    rw [neighbor_rankPointVertex_diagonal hside hj, rankPointVertex_mem_patch_iff,
+      mem_rankPatch]
+    rw [mem_rankPatch] at hpatch
+    rcases p with ⟨i, j, side⟩
+    simp [diagonalRankNeighbor, rankLevel] at hside hpatch ⊢
+    subst side
+    omega
+
+/-- A ranked dart is a listed patch contact exactly when its concrete dart is
+an A-based internal dart of the patch. -/
+theorem clippingRankDart_mem_aInternal_iff
+    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    {pd : RankPoint × Direction} :
+    pd ∈ patchContactDarts a b c ↔
+      clippingRankDartVertex pd ∈ aInternalDarts (patch a b c) := by
+  rcases pd with ⟨p, d⟩
+  cases d with
+  | same =>
+      constructor
+      · intro hpd
+        have hp : p ∈ sameContactPoints a b c := by
+          simpa [patchContactDarts] using hpd
+        have hpA := (Finset.mem_filter.mp hp).1
+        have hnot := (Finset.mem_filter.mp hp).2
+        apply Finset.mem_filter.mpr
+        refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+          ⟨rankPointVertex_mem_patch_iff.mpr (Finset.mem_filter.mp hpA).1,
+            Finset.mem_univ _⟩, ?_⟩, ?_⟩
+        · exact (clipping_same_neighbor_mem_iff ha hb hc hpA).mpr hnot
+        · simpa [clippingRankDartVertex, rankPointVertex] using
+            (Finset.mem_filter.mp hpA).2
+      · intro hint
+        rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+        rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+        have hpPatch := rankPointVertex_mem_patch_iff.mp
+          (Finset.mem_product.mp hprod).1
+        have hpA : p ∈ aRankPatch a b c := Finset.mem_filter.mpr
+          ⟨hpPatch, by simpa [clippingRankDartVertex, rankPointVertex] using hside⟩
+        have hp : p ∈ sameContactPoints a b c := Finset.mem_filter.mpr
+          ⟨hpA, (clipping_same_neighbor_mem_iff ha hb hc hpA).mp hn⟩
+        simpa [patchContactDarts] using hp
+  | horizontal =>
+      constructor
+      · intro hpd
+        have hp : p ∈ horizontalContactPoints a b c := by
+          simpa [patchContactDarts] using hpd
+        have hpA := (Finset.mem_filter.mp hp).1
+        have hnot := (Finset.mem_filter.mp hp).2
+        apply Finset.mem_filter.mpr
+        refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+          ⟨rankPointVertex_mem_patch_iff.mpr (Finset.mem_filter.mp hpA).1,
+            Finset.mem_univ _⟩,
+          (clipping_horizontal_neighbor_mem_iff ha hb hc hpA).mpr hnot⟩, ?_⟩
+        simpa [clippingRankDartVertex, rankPointVertex] using
+          (Finset.mem_filter.mp hpA).2
+      · intro hint
+        rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+        rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+        have hpPatch := rankPointVertex_mem_patch_iff.mp
+          (Finset.mem_product.mp hprod).1
+        have hpA : p ∈ aRankPatch a b c := Finset.mem_filter.mpr
+          ⟨hpPatch, by simpa [clippingRankDartVertex, rankPointVertex] using hside⟩
+        have hp : p ∈ horizontalContactPoints a b c := Finset.mem_filter.mpr
+          ⟨hpA, (clipping_horizontal_neighbor_mem_iff ha hb hc hpA).mp hn⟩
+        simpa [patchContactDarts] using hp
+  | diagonal =>
+      constructor
+      · intro hpd
+        have hp : p ∈ diagonalContactPoints a b c := by
+          simpa [patchContactDarts] using hpd
+        have hpA := (Finset.mem_filter.mp hp).1
+        have hnot := (Finset.mem_filter.mp hp).2
+        apply Finset.mem_filter.mpr
+        refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr
+          ⟨rankPointVertex_mem_patch_iff.mpr (Finset.mem_filter.mp hpA).1,
+            Finset.mem_univ _⟩,
+          (clipping_diagonal_neighbor_mem_iff ha hb hc hpA).mpr hnot⟩, ?_⟩
+        simpa [clippingRankDartVertex, rankPointVertex] using
+          (Finset.mem_filter.mp hpA).2
+      · intro hint
+        rcases Finset.mem_filter.mp hint with ⟨hint, hside⟩
+        rcases Finset.mem_filter.mp hint with ⟨hprod, hn⟩
+        have hpPatch := rankPointVertex_mem_patch_iff.mp
+          (Finset.mem_product.mp hprod).1
+        have hpA : p ∈ aRankPatch a b c := Finset.mem_filter.mpr
+          ⟨hpPatch, by simpa [clippingRankDartVertex, rankPointVertex] using hside⟩
+        have hp : p ∈ diagonalContactPoints a b c := Finset.mem_filter.mpr
+          ⟨hpA, (clipping_diagonal_neighbor_mem_iff ha hb hc hpA).mp hn⟩
+        simpa [patchContactDarts] using hp
+
+/-- The concrete neighbor of a listed ranked contact is its ranked B endpoint. -/
+theorem neighbor_clippingRankDart_eq
+    {a b c : ℕ} {pd : RankPoint × Direction}
+    (hpd : pd ∈ patchContactDarts a b c) :
+    neighbor (rankPointVertex pd.1) pd.2 = rankPointVertex (rankDartNeighbor pd) := by
+  rcases pd with ⟨p, d⟩
+  cases d with
+  | same =>
+      have hp : p ∈ sameContactPoints a b c := by
+        simpa [patchContactDarts] using hpd
+      exact neighbor_rankPointVertex_same
+        (Finset.mem_filter.mp (Finset.mem_filter.mp hp).1).2
+  | horizontal =>
+      have hp : p ∈ horizontalContactPoints a b c := by
+        simpa [patchContactDarts] using hpd
+      have hA := (Finset.mem_filter.mp hp).1
+      exact neighbor_rankPointVertex_horizontal
+        (Finset.mem_filter.mp hA).2
+        (Nat.pos_of_ne_zero (Finset.mem_filter.mp hp).2)
+  | diagonal =>
+      have hp : p ∈ diagonalContactPoints a b c := by
+        simpa [patchContactDarts] using hpd
+      have hA := (Finset.mem_filter.mp hp).1
+      exact neighbor_rankPointVertex_diagonal
+        (Finset.mem_filter.mp hA).2
+        (Nat.pos_of_ne_zero (Finset.mem_filter.mp hp).2)
+
+end OeisA263135
diff --git a/Scratch/A263135Ranks.lean b/Scratch/A263135Ranks.lean
new file mode 100644
index 0000000000..82f6e9a35d
--- /dev/null
+++ b/Scratch/A263135Ranks.lean
@@ -0,0 +1,86 @@
+import Scratch.A263135Staircase
+
+namespace OeisA263135
+
+/-- An occupied-row label attached to a vertex of `S`. -/
+def rowLabel (r : RowKind) (S : Finset Vertex) (v : ↥S) : ↥(occupiedRows r S) :=
+  ⟨rowCoord r v, Finset.mem_image.mpr ⟨v, v.property, rfl⟩⟩
+
+/-- Rank of a vertex's row among all occupied rows in the chosen direction. -/
+noncomputable def rowRank (r : RowKind) (S : Finset Vertex) (v : ↥S) :
+    Fin (occupiedRows r S).card :=
+  ((occupiedRows r S).orderIsoOfFin rfl).symm (rowLabel r S v)
+
+private theorem orderIso_rowRank (r : RowKind) (S : Finset Vertex) (v : ↥S) :
+    (occupiedRows r S).orderIsoOfFin rfl (rowRank r S v) = rowLabel r S v := by
+  exact ((occupiedRows r S).orderIsoOfFin rfl).apply_symm_apply _
+
+/-- Increasing row ranks imply increasing integer row coordinates. -/
+theorem rowCoord_le_of_rowRank_le (r : RowKind) (S : Finset Vertex) (v w : ↥S)
+    (h : rowRank r S v ≤ rowRank r S w) :
+    rowCoord r v ≤ rowCoord r w := by
+  have hmono := ((occupiedRows r S).orderIsoOfFin rfl).monotone h
+  simpa [orderIso_rowRank] using hmono
+
+/-- Equal row ranks are equivalent to equal row coordinates. -/
+theorem rowRank_eq_iff_rowCoord_eq (r : RowKind) (S : Finset Vertex) (v w : ↥S) :
+    rowRank r S v = rowRank r S w ↔ rowCoord r v = rowCoord r w := by
+  constructor
+  · intro h
+    have := congrArg (fun x : ↥(occupiedRows r S) => (x : ℤ))
+      (congrArg ((occupiedRows r S).orderIsoOfFin rfl) h)
+    simpa [orderIso_rowRank] using this
+  · intro h
+    apply ((occupiedRows r S).orderIsoOfFin rfl).symm.injective
+    apply Subtype.ext
+    exact h
+
+/-- The symmetric-chain index of a cell in an `a × b` rectangle. -/
+def rectangleChainIndex {a b : ℕ} (p : Fin a × Fin b) : ℕ :=
+  min p.1.val (b - 1 - p.2.val)
+
+/-- Points with the same rectangle-chain index are comparable coordinatewise. -/
+theorem rectangleChain_comparable {a b : ℕ} (p q : Fin a × Fin b)
+    (h : rectangleChainIndex p = rectangleChainIndex q) :
+    (p.1.val ≤ q.1.val ∧ p.2.val ≤ q.2.val) ∨
+      (q.1.val ≤ p.1.val ∧ q.2.val ≤ p.2.val) := by
+  rcases p with ⟨i, j⟩
+  rcases q with ⟨k, l⟩
+  unfold rectangleChainIndex at h
+  by_cases hi : i.val ≤ b - 1 - j.val
+  · rw [Nat.min_eq_left hi] at h
+    by_cases hk : k.val ≤ b - 1 - l.val
+    · rw [Nat.min_eq_left hk] at h
+      have hik : i.val = k.val := h
+      rcases le_total j.val l.val with hjl | hlj
+      · exact Or.inl ⟨hik.le, hjl⟩
+      · exact Or.inr ⟨hik.ge, hlj⟩
+    · rw [Nat.min_eq_right (Nat.le_of_not_ge hk)] at h
+      left
+      constructor <;> omega
+  · rw [Nat.min_eq_right (Nat.le_of_not_ge hi)] at h
+    by_cases hk : k.val ≤ b - 1 - l.val
+    · rw [Nat.min_eq_left hk] at h
+      right
+      constructor <;> omega
+    · rw [Nat.min_eq_right (Nat.le_of_not_ge hk)] at h
+      have hjl : j.val = l.val := by omega
+      rcases le_total i.val k.val with hik | hki
+      · exact Or.inl ⟨hik, hjl.le⟩
+      · exact Or.inr ⟨hki, hjl.ge⟩
+
+/-- The last grid point of its symmetric chain. -/
+def isRectangleChainLast {a b : ℕ} (p : Fin a × Fin b) : Prop :=
+  p.1.val = a - 1 ∧
+    p.2.val = b - 1 - rectangleChainIndex p
+
+instance {a b : ℕ} (p : Fin a × Fin b) : Decidable (isRectangleChainLast p) :=
+  inferInstance
+
+/-- The two chains obtained after multiplying a rectangle chain by the two honeycomb sides.
+`false` denotes the long chain (all `A` points plus the last `B` point); `true` denotes the short
+chain (all remaining `B` points). -/
+def boxSubchain {a b : ℕ} (p : Fin a × Fin b) (side : Bool) : Bool :=
+  side && decide (¬ isRectangleChainLast p)
+
+end OeisA263135
diff --git a/Scratch/A263135RowBound.lean b/Scratch/A263135RowBound.lean
new file mode 100644
index 0000000000..23d322b9dc
--- /dev/null
+++ b/Scratch/A263135RowBound.lean
@@ -0,0 +1,16 @@
+import Scratch.A263135Endpoints
+
+namespace OeisA263135
+
+/-- The edge boundary dominates the sum of the three occupied-row counts. -/
+theorem sum_occupiedRows_card_le_edgeBoundary (S : Finset Vertex) :
+    (∑ r : RowKind, (occupiedRows r S).card) ≤ edgeBoundary S := by
+  have hsum :
+      (∑ r : RowKind, 2 * (occupiedRows r S).card) ≤
+        ∑ r : RowKind, (rowBoundaryDarts r S).card := by
+    exact Finset.sum_le_sum fun r _ =>
+      two_mul_occupiedRows_card_le_rowBoundaryDarts_card r S
+  rw [sum_rowBoundaryDarts_card] at hsum
+  simpa [Finset.mul_sum] using Nat.le_of_mul_le_mul_left hsum
+
+end OeisA263135
diff --git a/Scratch/A263135Rows.lean b/Scratch/A263135Rows.lean
new file mode 100644
index 0000000000..0bc3bb1ae5
--- /dev/null
+++ b/Scratch/A263135Rows.lean
@@ -0,0 +1,82 @@
+import FormalConjectures.OEIS.«263135»
+
+namespace OeisA263135
+
+inductive RowKind
+  | first
+  | second
+  | diagonal
+  deriving DecidableEq, Fintype
+
+/-- The three integer row coordinates on the honeycomb graph. -/
+def rowCoord : RowKind → Vertex → ℤ
+  | .first, v => v.i
+  | .second, v => v.j
+  | .diagonal, v => v.i + v.j + if v.side then 1 else 0
+
+/-- A coordinate increasing by one along consecutive vertices of a fixed row. -/
+def alongCoord : RowKind → Vertex → ℤ
+  | .first, v => 2 * v.j + if v.side then 1 else 0
+  | .second, v => 2 * v.i + if v.side then 1 else 0
+  | .diagonal, v => 2 * v.i + if v.side then 1 else 0
+
+/-- The direction from `v` to the predecessor on a row. -/
+def prevDirection : RowKind → Vertex → Direction
+  | .first, ⟨_, _, false⟩ => .diagonal
+  | .first, ⟨_, _, true⟩ => .same
+  | .second, ⟨_, _, false⟩ => .horizontal
+  | .second, ⟨_, _, true⟩ => .same
+  | .diagonal, ⟨_, _, false⟩ => .horizontal
+  | .diagonal, ⟨_, _, true⟩ => .diagonal
+
+/-- The direction from `v` to the successor on a row. -/
+def nextDirection : RowKind → Vertex → Direction
+  | .first, ⟨_, _, false⟩ => .same
+  | .first, ⟨_, _, true⟩ => .diagonal
+  | .second, ⟨_, _, false⟩ => .same
+  | .second, ⟨_, _, true⟩ => .horizontal
+  | .diagonal, ⟨_, _, false⟩ => .diagonal
+  | .diagonal, ⟨_, _, true⟩ => .horizontal
+
+@[simp]
+theorem rowCoord_neighbor_prev (r : RowKind) (v : Vertex) :
+    rowCoord r (neighbor v (prevDirection r v)) = rowCoord r v := by
+  rcases v with ⟨i, j, side⟩
+  cases r <;> cases side <;> simp [rowCoord, prevDirection, neighbor]
+
+@[simp]
+theorem rowCoord_neighbor_next (r : RowKind) (v : Vertex) :
+    rowCoord r (neighbor v (nextDirection r v)) = rowCoord r v := by
+  rcases v with ⟨i, j, side⟩
+  cases r <;> cases side <;> simp [rowCoord, nextDirection, neighbor]
+
+@[simp]
+theorem alongCoord_neighbor_prev (r : RowKind) (v : Vertex) :
+    alongCoord r (neighbor v (prevDirection r v)) = alongCoord r v - 1 := by
+  rcases v with ⟨i, j, side⟩
+  cases r <;> cases side <;> simp [alongCoord, prevDirection, neighbor]
+
+@[simp]
+theorem alongCoord_neighbor_next (r : RowKind) (v : Vertex) :
+    alongCoord r (neighbor v (nextDirection r v)) = alongCoord r v + 1 := by
+  rcases v with ⟨i, j, side⟩
+  cases r <;> cases side <;> simp [alongCoord, nextDirection, neighbor]
+
+@[simp]
+theorem prevDirection_ne_nextDirection (r : RowKind) (v : Vertex) :
+    prevDirection r v ≠ nextDirection r v := by
+  rcases v with ⟨i, j, side⟩
+  cases r <;> cases side <;> decide
+
+/-- Directed boundary incidences of a finite honeycomb set. -/
+def boundaryDarts (S : Finset Vertex) : Finset (Vertex × Direction) :=
+  (S ×ˢ Finset.univ).filter fun vd => neighbor vd.1 vd.2 ∉ S
+
+/-- Number of directed edges from `S` to its complement. -/
+def edgeBoundary (S : Finset Vertex) : ℕ := (boundaryDarts S).card
+
+/-- The set of row labels occupied by `S` in one of the three directions. -/
+def occupiedRows (r : RowKind) (S : Finset Vertex) : Finset ℤ :=
+  S.image (rowCoord r)
+
+end OeisA263135
diff --git a/Scratch/A263135Staircase.lean b/Scratch/A263135Staircase.lean
new file mode 100644
index 0000000000..6d120bfecb
--- /dev/null
+++ b/Scratch/A263135Staircase.lean
@@ -0,0 +1,82 @@
+import Scratch.A263135RowBound
+
+namespace OeisA263135
+
+/-- Sum of the positive terms in the arithmetic progression `q, q-2, q-4, ...`. -/
+def staircase (q : ℕ) : ℕ :=
+  ∑ t ∈ Finset.range q, q - 2 * t
+
+private theorem staircase_add_two (q : ℕ) :
+    staircase (q + 2) = staircase q + q + 2 := by
+  unfold staircase
+  rw [Finset.sum_range_succ']
+  simp only [Nat.mul_zero, Nat.sub_zero]
+  have hshift :
+      (∑ t ∈ Finset.range (q + 1), q + 2 - 2 * (t + 1)) =
+        ∑ t ∈ Finset.range (q + 1), q - 2 * t := by
+    apply Finset.sum_congr rfl
+    intro t ht
+    omega
+  rw [hshift, Finset.sum_range_succ]
+  have hlast : q - 2 * q = 0 := by omega
+  simp [hlast]
+  omega
+
+private theorem staircase_eq_sub_add : ∀ q : ℕ,
+    staircase q = staircase (q - 2) + q
+  | 0 => by simp [staircase]
+  | 1 => by norm_num [staircase]
+  | q + 2 => by
+      simpa only [Nat.add_sub_cancel] using staircase_add_two q
+
+/-- Deficiency contributed by the two symmetric chains over one grid-chain family. -/
+def staircaseDeficiency (q : ℕ) : ℕ :=
+  staircase q + staircase (q - 2)
+
+private theorem staircaseDeficiency_add_two (q : ℕ) :
+    staircaseDeficiency (q + 2) = staircaseDeficiency q + 2 * q + 2 := by
+  rw [staircaseDeficiency, staircaseDeficiency, Nat.add_sub_cancel,
+    staircase_add_two, staircase_eq_sub_add q]
+  omega
+
+/-- Twice the staircase deficiency dominates the square of its width. -/
+theorem sq_le_two_mul_staircaseDeficiency : ∀ q : ℕ,
+    q ^ 2 ≤ 2 * staircaseDeficiency q
+  | 0 => by simp [staircaseDeficiency, staircase]
+  | 1 => by norm_num [staircaseDeficiency, staircase]
+  | q + 2 => by
+      have ih := sq_le_two_mul_staircaseDeficiency q
+      rw [staircaseDeficiency_add_two]
+      nlinarith
+
+/-- The purely arithmetic implication used after the chain count. -/
+theorem perimeter_square_of_chain_deficiency
+    (a b c m : ℕ)
+    (hab : a ≤ b)
+    (hbc : b ≤ c)
+    (hm : m + staircaseDeficiency (a + b - c) ≤ 2 * a * b) :
+    6 * m ≤ (a + b + c) ^ 2 := by
+  let q := a + b - c
+  have hq : q ≤ a := by
+    dsimp [q]
+    omega
+  have hc : a + b = c + q := by
+    dsimp [q]
+    omega
+  have hsq := sq_le_two_mul_staircaseDeficiency q
+  have hm2 : 2 * m + q ^ 2 ≤ 4 * a * b := by
+    nlinarith
+  let x := a - q
+  let z := b - a
+  have haeq : a = q + x := by
+    dsimp [x]
+    omega
+  have hbeq : b = q + x + z := by
+    dsimp [x, z]
+    omega
+  have hceq : c = q + 2 * x + z := by
+    omega
+  rw [haeq, hbeq, hceq] at hm2 ⊢
+  nlinarith [Nat.zero_le (x ^ 2), Nat.zero_le (x * z), Nat.zero_le (z ^ 2)]
+
+end OeisA263135
diff --git a/Scratch/A263135Symmetry.lean b/Scratch/A263135Symmetry.lean
new file mode 100644
index 0000000000..7dc259efcc
--- /dev/null
+++ b/Scratch/A263135Symmetry.lean
@@ -0,0 +1,165 @@
+import Scratch.A263135CapArithmetic
+
+namespace OeisA263135
+
+/-- Reflection interchanging the first two row directions. -/
+def swapVertex (v : Vertex) : Vertex := ⟨v.j, v.i, v.side⟩
+
+@[simp]
+theorem swapVertex_involutive (v : Vertex) : swapVertex (swapVertex v) = v := by
+  rcases v with ⟨i, j, side⟩
+  rfl
+
+theorem swapVertex_injective : Function.Injective swapVertex :=
+  Function.LeftInverse.injective swapVertex_involutive
+
+/-- A 120-degree lattice rotation.  On row coordinates it sends
+`(first, second, diagonal)` to `(diagonal, first, second)`, up to signs. -/
+def rotateVertex : Vertex → Vertex
+  | ⟨i, j, false⟩ => ⟨-i - j, i, false⟩
+  | ⟨i, j, true⟩ => ⟨-i - j - 1, i, true⟩
+
+theorem rotateVertex_injective : Function.Injective rotateVertex := by
+  intro v w h
+  rcases v with ⟨i, j, side⟩
+  rcases w with ⟨k, l, side'⟩
+  cases side <;> cases side' <;> simp [rotateVertex] at h ⊢ <;> omega
+
+/-- Negation of a finite set of integer row labels. -/
+def negRows (T : Finset ℤ) : Finset ℤ := T.image fun x => -x
+
+@[simp]
+theorem card_negRows (T : Finset ℤ) : (negRows T).card = T.card := by
+  exact Finset.card_image_of_injective T neg_injective
+
+@[simp]
+theorem rowCoord_swap_first (v : Vertex) :
+    rowCoord .first (swapVertex v) = rowCoord .second v := by
+  rfl
+
+@[simp]
+theorem rowCoord_swap_second (v : Vertex) :
+    rowCoord .second (swapVertex v) = rowCoord .first v := by
+  rfl
+
+@[simp]
+theorem rowCoord_swap_diagonal (v : Vertex) :
+    rowCoord .diagonal (swapVertex v) = rowCoord .diagonal v := by
+  rcases v with ⟨i, j, side⟩
+  cases side <;> simp [swapVertex, rowCoord, add_comm]
+
+@[simp]
+theorem rowCoord_rotate_first (v : Vertex) :
+    rowCoord .first (rotateVertex v) = -rowCoord .diagonal v := by
+  rcases v with ⟨i, j, side⟩
+  cases side <;> simp [rotateVertex, rowCoord] <;> ring
+
+@[simp]
+theorem rowCoord_rotate_second (v : Vertex) :
+    rowCoord .second (rotateVertex v) = rowCoord .first v := by
+  rcases v with ⟨i, j, side⟩
+  cases side <;> rfl
+
+@[simp]
+theorem rowCoord_rotate_diagonal (v : Vertex) :
+    rowCoord .diagonal (rotateVertex v) = -rowCoord .second v := by
+  rcases v with ⟨i, j, side⟩
+  cases side <;> simp [rotateVertex, rowCoord] <;> ring
+
+@[simp]
+theorem card_image_swapVertex (S : Finset Vertex) :
+    (S.image swapVertex).card = S.card := by
+  exact Finset.card_image_of_injective S swapVertex_injective
+
+@[simp]
+theorem card_image_rotateVertex (S : Finset Vertex) :
+    (S.image rotateVertex).card = S.card := by
+  exact Finset.card_image_of_injective S rotateVertex_injective
+
+@[simp]
+theorem occupiedRows_swap_first (S : Finset Vertex) :
+    occupiedRows .first (S.image swapVertex) = occupiedRows .second S := by
+  ext x
+  simp [occupiedRows]
+
+@[simp]
+theorem occupiedRows_swap_second (S : Finset Vertex) :
+    occupiedRows .second (S.image swapVertex) = occupiedRows .first S := by
+  ext x
+  simp [occupiedRows]
+
+@[simp]
+theorem occupiedRows_swap_diagonal (S : Finset Vertex) :
+    occupiedRows .diagonal (S.image swapVertex) = occupiedRows .diagonal S := by
+  ext x
+  simp [occupiedRows]
+
+@[simp]
+theorem occupiedRows_rotate_first (S : Finset Vertex) :
+    occupiedRows .first (S.image rotateVertex) = negRows (occupiedRows .diagonal S) := by
+  ext x
+  constructor
+  · intro hx
+    rcases Finset.mem_image.mp hx with ⟨v, hv, rfl⟩
+    rcases Finset.mem_image.mp hv with ⟨w, hw, rfl⟩
+    exact Finset.mem_image.mpr
+      ⟨rowCoord .diagonal w, Finset.mem_image.mpr ⟨w, hw, rfl⟩, by simp⟩
+  · intro hx
+    rcases Finset.mem_image.mp hx with ⟨z, hz, rfl⟩
+    rcases Finset.mem_image.mp hz with ⟨w, hw, rfl⟩
+    exact Finset.mem_image.mpr
+      ⟨rotateVertex w, Finset.mem_image.mpr ⟨w, hw, rfl⟩, by simp⟩
+
+@[simp]
+theorem occupiedRows_rotate_second (S : Finset Vertex) :
+    occupiedRows .second (S.image rotateVertex) = occupiedRows .first S := by
+  ext x
+  simp [occupiedRows]
+
+@[simp]
+theorem occupiedRows_rotate_diagonal (S : Finset Vertex) :
+    occupiedRows .diagonal (S.image rotateVertex) = negRows (occupiedRows .second S) := by
+  ext x
+  constructor
+  · intro hx
+    rcases Finset.mem_image.mp hx with ⟨v, hv, rfl⟩
+    rcases Finset.mem_image.mp hv with ⟨w, hw, rfl⟩
+    exact Finset.mem_image.mpr
+      ⟨rowCoord .second w, Finset.mem_image.mpr ⟨w, hw, rfl⟩, by simp⟩
+  · intro hx
+    rcases Finset.mem_image.mp hx with ⟨z, hz, rfl⟩
+    rcases Finset.mem_image.mp hz with ⟨w, hw, rfl⟩
+    exact Finset.mem_image.mpr
+      ⟨rotateVertex w, Finset.mem_image.mpr ⟨w, hw, rfl⟩, by simp⟩
+
+/-- The quadratic row-count inequality, with no ordering assumption. -/
+theorem six_mul_card_le_row_sum_sq (S : Finset Vertex) :
+    6 * S.card ≤
+      ((occupiedRows .first S).card + (occupiedRows .second S).card +
+        (occupiedRows .diagonal S).card) ^ 2 := by
+  let a := (occupiedRows .first S).card
+  let b := (occupiedRows .second S).card
+  let c := (occupiedRows .diagonal S).card
+  rcases le_total a b with hab | hba
+  · rcases le_total b c with hbc | hcb
+    · exact six_mul_card_le_row_sum_sq_of_sorted S hab hbc
+    · rcases le_total a c with hac | hca
+      · have h := six_mul_card_le_row_sum_sq_of_sorted
+          ((S.image rotateVertex).image swapVertex) (by simpa [a, c]) (by simpa [b, c])
+        simpa [a, b, c, add_assoc, add_left_comm, add_comm] using h
+      · have h := six_mul_card_le_row_sum_sq_of_sorted
+          (S.image rotateVertex) (by simpa [a, c]) (by simpa [a, b])
+        simpa [a, b, c, add_assoc, add_left_comm, add_comm] using h
+  · rcases le_total a c with hac | hca
+    · have h := six_mul_card_le_row_sum_sq_of_sorted
+        (S.image swapVertex) (by simpa [a, b]) (by simpa [a, c])
+      simpa [a, b, c, add_assoc, add_left_comm, add_comm] using h
+    · rcases le_total b c with hbc | hcb
+      · let T := (S.image rotateVertex).image rotateVertex
+        have h := six_mul_card_le_row_sum_sq_of_sorted T (by simpa [T, b, c]) (by simpa [T, a, c])
+        simpa [T, a, b, c, add_assoc, add_left_comm, add_comm] using h
+      · let T := ((S.image rotateVertex).image rotateVertex).image swapVertex
+        have h := six_mul_card_le_row_sum_sq_of_sorted T (by simpa [T, b, c]) (by simpa [T, a, b])
+        simpa [T, a, b, c, add_assoc, add_left_comm, add_comm] using h
+
+end OeisA263135
diff --git a/Scratch/A263135Upper.lean b/Scratch/A263135Upper.lean
new file mode 100644
index 0000000000..8dbac2003d
--- /dev/null
+++ b/Scratch/A263135Upper.lean
@@ -0,0 +1,55 @@
+import Scratch.A263135Incidence
+
+namespace OeisA263135
+
+/-- The edge boundary of an even-cardinality honeycomb set is even. -/
+theorem edgeBoundary_even_of_card_eq_two_mul
+    (S : Finset Vertex) (n : ℕ) (hcard : S.card = 2 * n) :
+    Even (edgeBoundary S) := by
+  have hinc := three_mul_card_eq_two_mul_contacts_add_boundary S
+  rw [hcard] at hinc
+  have hc : contacts S ≤ 3 * n := by omega
+  refine ⟨3 * n - contacts S, ?_⟩
+  omega
+
+/-- Boundary lower bound at even cardinality. -/
+theorem two_mul_ceilSqrt_le_edgeBoundary
+    (S : Finset Vertex) (n r : ℕ)
+    (hcard : S.card = 2 * n)
+    (hr : IsNatCeilSqrt (3 * n) r) :
+    2 * r ≤ edgeBoundary S := by
+  let R := (occupiedRows .first S).card + (occupiedRows .second S).card +
+    (occupiedRows .diagonal S).card
+  have hrow : R ≤ edgeBoundary S := by
+    simpa [R] using sum_occupiedRows_card_le_edgeBoundary S
+  have hquad := six_mul_card_le_row_sum_sq S
+  rw [hcard] at hquad
+  have hboundarySq : 12 * n ≤ (edgeBoundary S) ^ 2 := by
+    have hsq : R ^ 2 ≤ (edgeBoundary S) ^ 2 := by
+      nlinarith
+    nlinarith
+  rcases edgeBoundary_even_of_card_eq_two_mul S n hcard with ⟨q, hq⟩
+  have hqSq : 3 * n ≤ q ^ 2 := by
+    rw [hq] at hboundarySq
+    nlinarith
+  have hrq : r ≤ q := by
+    by_contra h
+    have hqr : q ≤ r - 1 := by omega
+    have hsquares : q ^ 2 ≤ (r - 1) ^ 2 := by
+      nlinarith
+    exact (not_lt_of_ge (hqSq.trans hsquares)) hr.1
+  rw [hq]
+  omega
+
+/-- Universal half of the even-index A263135 closed form. -/
+theorem contacts_le_even_closed_form
+    (S : Finset Vertex) (n r : ℕ)
+    (hcard : S.card = 2 * n)
+    (hr : IsNatCeilSqrt (3 * n) r) :
+    contacts S ≤ 3 * n - r := by
+  have hboundary := two_mul_ceilSqrt_le_edgeBoundary S n r hcard hr
+  have hinc := three_mul_card_eq_two_mul_contacts_add_boundary S
+  rw [hcard] at hinc
+  omega
+
+end OeisA263135
diff --git a/lakefile.toml b/lakefile.toml
index f80df988b5..10a14d4cda 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -11,7 +11,7 @@
 
 name = "formal_conjectures"
 keywords = ["math"]
-defaultTargets = ["FormalConjectures"]
+defaultTargets = ["FormalConjectures", "A263135ScratchAudit"]
 testDriver = "FormalConjecturesTest"
 
 [leanOptions]
@@ -33,9 +33,6 @@ rev = "v4.27.0"
 [[lean_lib]]
 name = "FormalConjecturesForMathlib"
 
-[[lean_lib]]
-name = "FormalConjecturesUtil"
-
 [[lean_lib]]
 name = "FormalConjecturesTest"
 [lean_lib.leanOptions]
@@ -53,6 +50,16 @@ weak.linter.style.ams_attribute = true
 weak.linter.style.category_attribute = true
 weak.linter.style.moduleDocstring = true
 
+# Focused temporary library for the OEIS A263135 proof workbench.
+# Building this exact root compiles its complete transitive scratch dependency stack.
+[[lean_lib]]
+name = "A263135ScratchAudit"
+globs = ["Scratch.A263135Audit"]
+
+# Fork-hosted complete Lean proofs that are linked from upstream metadata.
+[[lean_lib]]
+name = "WOWII"
+
 [[lean_lib]]
 name = "FormalConjecturesAnswerPostpone"
 globs = ["FormalConjectures.+"]