edge_deviation_small
plain-language theorem explainer
If the J-cost of a positive ratio r is at most δ with δ ≤ 1, then the squared deviation from unity obeys (r-1)^2 ≤ 8δ. Workers on approximate holography and perturbation bounds in Recognition Science cite this to control field variation on graphs when exact J-minima are unavailable. The proof is a short calculation that tightens the general edge deviation bound by replacing 1+δ with 2 under the δ ≤ 1 hypothesis.
Claim. Let $J$ be the cost function. For $r > 0$, $0 ≤ δ ≤ 1$, if $J(r) ≤ δ$ then $(r-1)^2 ≤ 8δ$.
background
The Approximate Holography module shows that near-J-minimum configurations on connected graphs remain approximately holographic, with field variation bounded by edge costs. Jcost r is the Recognition cost J(r) = (r + r^{-1})/2 - 1 derived from the Recognition Composition Law; small Jcost values quantify how far a ratio deviates from the fixed point 1. The module closes Gap G2 in the brain holography chain by replacing the exact J=0 assumption with explicit perturbation bounds.
proof idea
Apply the upstream edge_deviation_bound lemma to obtain (r-1)^2 ≤ 4δ(1+δ). Under the hypothesis δ ≤ 1, nlinarith replaces the factor (1+δ) by 2. Ring simplification then yields the target 8δ.
why it matters
This result is invoked by abs_deviation_small to extract the absolute bound |r-1| ≤ √(8δ), by continuity_in_delta to establish continuous degradation of holography with δ, and by perturbation_certificate as part of the complete perturbation package. It feeds directly into brain_holography_fully_forced, supplying the approximate-case step that closes the perturbation gap between RCL and holographic constancy. The bound corresponds to the δ-small regime in the GCIC framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.