perturbation_certificate
plain-language theorem explainer
A complete set of perturbation bounds shows that small deviations from J-minimum control squared field variations on connected graphs, recovering exact constancy at zero deviation. Researchers modeling approximate holography in recognition-based systems would cite these results to extend exact rigidity theorems to realistic near-minimum configurations. The proof assembles the three component bounds via a direct conjunction of prior deviation lemmas.
Claim. Let $J(r) = (r + r^{-1})/2 - 1$ for $r > 0$. The following hold simultaneously: (i) for all $r > 0$ and all $δ ≥ 0$, if $J(r) ≤ δ$ then $(r-1)^2 ≤ 4δ(1+δ)$; (ii) for all $r > 0$ and all $δ$ with $0 ≤ δ ≤ 1$, if $J(r) ≤ δ$ then $(r-1)^2 ≤ 8δ$; (iii) on any connected graph $(V, adj)$ with positive values $x: V → ℝ$, if $J(x_v/x_w) ≤ 0$ for every adjacent pair then $x$ is constant.
background
The module develops approximate holography from near-J-minimum configurations, proving that field variation across a connected graph remains controlled by edge costs when the system sits close to but not exactly at J=0. This replaces the exact J=0 assumption of prior rigidity results and closes Gap G2 in the brain holography argument. Jcost is the recognition cost function obeying the Recognition Composition Law, with the explicit form $J(r) = (r + r^{-1})/2 - 1$ for positive $r$.
proof idea
The proof is a one-line wrapper that refines the goal into a three-way conjunction and discharges each conjunct by direct application of an upstream result: edge_deviation_bound for the general quadratic bound, edge_deviation_small for the tightened linear bound when $δ ≤ 1$, and exact_case_recovery for the exact constancy statement at $δ = 0$.
why it matters
This declaration supplies the complete perturbation certificate that closes Gap G2 in the brain holography proof, allowing realistic systems with small nonzero J-cost. It feeds the approximate-holography package by combining the edge-deviation bounds with exact recovery, supporting the transition from exact J-uniqueness in the forcing chain to controlled deviations on graphs. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.