exact_case_recovery
plain-language theorem explainer
When the J-cost on adjacent edges is non-positive, a positive field on a connected graph must be constant. Researchers working on approximate holography cite this result to recover exact GCIC rigidity from the zero-perturbation limit. The argument first forces each edge cost to zero by combining the non-positivity hypothesis with Jcost non-negativity, then invokes ratio rigidity on the connected graph.
Claim. Let $J$ be the J-cost function. Suppose $(V, adj)$ is a graph such that the adjacency relation is connected (its reflexive transitive closure relates every pair of vertices), $x: V → ℝ$ satisfies $x(v) > 0$ for every vertex $v$, and $J(x(v)/x(w)) ≤ 0$ for every adjacent pair. Then $x(v) = x(w)$ for all vertices $v, w$.
background
J-cost is the non-negative function $J(r) = (r + r^{-1})/2 - 1$ for $r > 0$, with equality if and only if $r = 1$ (AM-GM). The upstream lemma Jcost_nonneg states that $J(r) ≥ 0$ whenever $r > 0$. GraphRigidity.ratio_rigidity is the lemma that zero J-cost on every edge of a connected graph forces the field to be constant. The module ApproximateHolography proves that near-minimum J-cost configurations remain approximately holographic, closing Gap G2 by replacing the exact J = 0 assumption with a controlled perturbation.
proof idea
The tactic proof first constructs an auxiliary fact that Jcost(x v / x w) = 0 on every edge: the given inequality Jcost ≤ 0 is combined with Jcost_nonneg (applied to the positive ratio) and discharged by linarith. The resulting zero-cost hypothesis is then fed directly to the upstream theorem GraphRigidity.ratio_rigidity together with connectivity and positivity, which yields the required constancy.
why it matters
exact_case_recovery recovers exact GCIC rigidity when the perturbation parameter δ vanishes, supplying the base case for the continuity statement continuity_in_delta and the full perturbation_certificate. It closes Gap G2 in the brain holography argument by showing that the exact J = 0 condition implies field constancy on connected graphs. Within the Recognition Science chain it instantiates T5 (J-uniqueness) in the holographic setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.