edge_deviation_bound
plain-language theorem explainer
If Jcost(r) ≤ δ for r > 0 and δ ≥ 0, then (r-1)^2 ≤ 4δ(1+δ). Researchers analyzing approximate graph rigidity and near-minimum holographic configurations cite this to control edge deviations under small J-cost perturbations. The proof invokes the quadratic deviation lemma to reach (r-1)^2 ≤ 2rδ, substitutes the derived upper bound r ≤ 2+2δ, and closes via nlinarith followed by ring simplification.
Claim. For $r > 0$ and $δ ≥ 0$, if $J(r) ≤ δ$ then $(r-1)^2 ≤ 4δ(1+δ)$.
background
The module develops bounds for configurations near (but not exactly at) J=0, showing that field variation across a connected graph remains controlled by edge costs. This replaces the exact J=0 assumption with a perturbation bound, closing Gap G2 in the brain holography proof. Jcost denotes the per-edge cost function whose small values enforce near-rigidity; the upstream lemma sq_deviation_le_of_Jcost_le states that Jcost(x) ≤ δ and x > 0 imply (x-1)^2 ≤ 2xδ. The companion lemma upper_bound_of_Jcost_le states that the same hypotheses imply x ≤ 2 + 2δ.
proof idea
The proof applies sq_deviation_le_of_Jcost_le to obtain (r-1)^2 ≤ 2rδ. It then applies upper_bound_of_Jcost_le to replace r by the bound 2+2δ. The resulting inequality 2rδ ≤ 2(2+2δ)δ is simplified by nlinarith, after which ring rearranges the right-hand side to 4δ(1+δ).
why it matters
This supplies the general bound specialized by edge_deviation_small to (r-1)^2 ≤ 8δ when δ ≤ 1 and packaged with that case in perturbation_certificate. It directly supports the module claim that near-J-minimum graphs remain approximately holographic, extending exact rigidity (recovered when δ=0) to realistic systems. In the Recognition framework it bridges T5 J-uniqueness to small-defect regimes while preserving the RCL structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.