continuity_in_delta
plain-language theorem explainer
The theorem establishes that holographic constancy on connected graphs holds exactly at zero J-cost and degrades continuously for small positive deviations δ. Researchers modeling near-minimum configurations in recognition-based holography cite it to replace exact J=0 assumptions with controlled perturbations. The proof is a one-line wrapper that splits the conjunction and invokes the exact recovery lemma for δ=0 together with the small-deviation bound for δ≤1.
Claim. Let $G$ be a connected graph with positive real vertex weights $x_v$. If $J(x_v/x_w)≤0$ for every edge then $x$ is constant. Moreover, for $r>0$ and $δ∈[0,1]$, $J(r)≤δ$ implies $(r-1)^2≤8δ$.
background
The module proves that configurations near but not exactly at J=0 remain approximately holographic: field variation across a connected graph is controlled by edge costs. Jcost is the recognition cost function whose zero set forces self-similarity. The exact_case_recovery result states that Jcost≤0 on a connected graph with positive weights recovers exact constancy. The edge_deviation_small result supplies the quadratic bound $(r-1)^2≤8δ$ when δ≤1. This local setting closes Gap G2 by replacing the exact J=0 hypothesis of GCIC rigidity with a perturbation that covers realistic systems.
proof idea
The term proof applies constructor to split the conjunction. The first conjunct is discharged by direct application of exact_case_recovery to the connectedness, positivity, and cost hypotheses. The second conjunct is discharged by direct application of edge_deviation_small to the supplied r, δ, and Jcost inequality.
why it matters
The declaration completes the perturbation analysis package by linking exact GCIC rigidity recovery to the continuous deviation bound. It fills the transition step required for the brain holography proof, allowing small nonzero J-cost to preserve approximate holography. The result supports the framework claim that holography emerges continuously from near-J-minimum states on the recognition manifold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.