upper_bound_of_Jcost_le
plain-language theorem explainer
If the J-cost of a positive real x is at most δ ≥ 0, then x ≤ 2 + 2δ. Researchers deriving approximate holographic bounds on graph edges in Recognition Science cite this to control deviations from the J-minimum. The proof is by contradiction: the assumption x > 2 + 2δ produces a strict lower bound on (x-1)^2 that contradicts the upper bound (x-1)^2 ≤ 2xδ supplied by the companion lemma sq_deviation_le_of_Jcost_le, with the final step via nlinarith.
Claim. Let $x > 0$ and $δ ≥ 0$ be real numbers. If the J-cost satisfies Jcost(x) ≤ δ, then $x ≤ 2 + 2δ$.
background
The Approximate Holography module shows that near-J-minimum configurations remain approximately holographic, with field variation across a connected graph controlled by edge costs. The J-cost is the function satisfying Jcost(x) = (x-1)^2 / (2x) for x > 0, recovered by rewriting the hypothesis in the companion lemma. The module replaces the exact J=0 assumption with a small-δ perturbation to close Gap G2 in the brain holography argument, yielding continuous degradation of the holographic property with δ.
proof idea
The tactic proof assumes for contradiction that x > 2 + 2δ, derives x-1 > 1 + 2δ, and obtains the strict inequality (1 + 2δ)^2 < (x-1)^2 by squaring. It then invokes sq_deviation_le_of_Jcost_le to replace the right-hand side by the upper bound 2xδ, producing (1 + 2δ)^2 < 2xδ. The final nlinarith step with sq_nonneg δ yields the contradiction.
why it matters
This lemma supplies the linear upper bound on x required to convert the quadratic deviation inequality into the final edge deviation bound. It is invoked directly by edge_deviation_bound to obtain (r-1)^2 ≤ 4δ(1+δ). Within the Recognition Science framework it supports the approximate-holography results that close Gap G2, extending the J-uniqueness property (T5) to quantitative control away from the exact minimum while preserving the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.