sq_deviation_le_of_Jcost_le
plain-language theorem explainer
If J(x) ≤ δ with x positive, the squared deviation from unity is at most 2xδ. Workers on approximate holography cite this to bound deviations in near-minimal configurations. The proof substitutes the squared expression for Jcost and rearranges the resulting inequality by multiplying through by the positive factor 2x.
Claim. If $J(x) ≤ δ$ and $x > 0$, then $(x-1)^2 ≤ 2xδ$.
background
Jcost is the Recognition cost J(x) = (x + x^{-1})/2 - 1, equivalently (x-1)^2/(2x) for x ≠ 0 by the upstream lemma Jcost_eq_sq. The module Approximate Holography 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 closes Gap G2 by replacing the exact J=0 assumption with a perturbation bound that covers realistic systems.
proof idea
The proof invokes Jcost_eq_sq to rewrite the hypothesis Jcost x ≤ δ as (x-1)^2/(2x) ≤ δ. It then rewrites (x-1)^2 as that quotient times 2x, applies mul_le_mul_of_nonneg_right using positivity of 2x, and finishes with ring to obtain the target bound.
why it matters
This lemma supplies the core inequality for edge_deviation_bound, which upgrades it to (r-1)^2 ≤ 4δ(1+δ) and thereby supports continuity_in_delta and exact_case_recovery. It fills the step from exact GCIC rigidity to approximate holography in near-minimal systems, directly addressing Gap G2 in the brain holography proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.