abs_deviation_small
plain-language theorem explainer
Researchers studying approximate holography in Recognition Science cite this bound to control deviations from exact rigidity when J-cost is small but positive. If J(r) ≤ δ with r > 0 and 0 ≤ δ ≤ 1, then |r - 1| ≤ √(8δ). The proof is a short tactic sequence that applies the squared deviation lemma and invokes square-root monotonicity after confirming non-negativity.
Claim. If $J(r) ≤ δ$ for $r > 0$ and $0 ≤ δ ≤ 1$, then $|r - 1| ≤ √(8δ)$.
background
The module proves that configurations near (but not exactly at) J=0 are approximately holographic: field variation across a connected graph is controlled by edge costs. This replaces the exact J=0 assumption with a perturbation bound, closing Gap G2 in the brain holography proof. J-cost is the functional J(r) = (r + r^{-1})/2 - 1 from the Cost module. The upstream theorem edge_deviation_small states that for δ ≤ 1 the squared deviation satisfies (r-1)^2 ≤ 8δ under the same hypotheses.
proof idea
The proof applies edge_deviation_small to obtain (r-1)^2 ≤ 8δ. It confirms 8δ ≥ 0 by nlinarith, rewrites the target bound as √((r-1)^2) via the identity √(x^2) = |x|, applies Real.sqrt_le_sqrt, and reduces via sq_abs to the squared result.
why it matters
This supplies the absolute deviation form required for the approximate holography framework and directly supports continuity_in_delta together with exact_case_recovery when δ=0. It fills the perturbation step linking T5 J-uniqueness to holographic control in Recognition Science, replacing exact minima with a bound usable for realistic systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.