edge_deviation_bound
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.
claimFor $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 in Recognition Science
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.
scope and limits
- Does not apply for r ≤ 0.
- Does not yield a δ-independent bound.
- Does not address multi-edge composition without further lemmas.
- Does not claim exact holography for δ > 0.
formal statement (Lean)
59theorem edge_deviation_bound {r : ℝ} (hr : 0 < r) {δ : ℝ} (hδ : 0 ≤ δ)
60 (hJ : Jcost r ≤ δ) : (r - 1) ^ 2 ≤ 4 * δ * (1 + δ) := by
proof body
Tactic-mode proof.
61 have hsq := sq_deviation_le_of_Jcost_le hr hδ hJ
62 have hub := upper_bound_of_Jcost_le hr hδ hJ
63 calc (r - 1) ^ 2 ≤ 2 * r * δ := hsq
64 _ ≤ 2 * (2 + 2 * δ) * δ := by nlinarith
65 _ = 4 * δ * (1 + δ) := by ring
66
67/-- For small δ (≤ 1), the edge deviation simplifies to (r-1)² ≤ 8δ. -/