global_minimum_unique
plain-language theorem explainer
The theorem shows that J-cost vanishes exactly at the point x=1 for every positive real argument. Workers on R-hat attractors and fixed-point convergence in Recognition Science lattices cite it to lock down uniqueness of the zero-defect state. The tactic proof splits the biconditional, rewrites via the squared form of J-cost, rules out a positive square by contradiction and linarith, and invokes the direct evaluation lemma for the converse.
Claim. For every real number $x > 0$, the J-cost function satisfies $J(x) = 0$ if and only if $x = 1$.
background
The module treats R-hat as a J-cost contraction on finite lattices whose fixed points determine the thought vocabulary of the intelligence. J-cost is the function given by the squared ratio $J(x) = (x-1)^2/(2x)$ for $x ≠ 0$, supplied by the lemma Jcost_eq_sq; its vanishing at unity follows at once from the companion lemma Jcost_unit0. The local setting is the existence-uniqueness theory for R-hat attractors, which includes the results contraction_has_fixed_point, fixed_point_is_jcost_minimum, and local_minima_from_topology.
proof idea
The proof opens the biconditional with constructor. The forward direction rewrites the hypothesis with Jcost_eq_sq, assumes by contradiction that $(x-1)^2 > 0$, obtains a strictly positive quotient, and reaches a contradiction by linarith. The reverse direction substitutes $x=1$ and applies Jcost_unit0 directly.
why it matters
The result establishes uniqueness of the global J-cost minimum at the defect-free state $x=1$, which supports the identification of fixed points with local minima. It fills the unique_global_minimum slot inside the R-hat fixed-point theory of the module and aligns with the J-uniqueness property in the forcing chain. The theorem therefore anchors the claim that contractions on finite graphs converge to a single attractor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.