J_cost_minimum_at_one
plain-language theorem explainer
The J-cost function attains its global minimum value of zero at argument one. Condensed matter modelers in the Recognition framework cite this to anchor the zero-energy reference for phase transition calculations. The proof is a one-line wrapper that unfolds the definition and evaluates the resulting arithmetic expression to zero.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for real $x > 0$. Then $J(1) = 0$.
background
The J-cost function is defined by the expression $J(x) = (x + x^{-1})/2 - 1$. This module studies its role in condensed-matter phase transitions, with the function serving as the canonical cost measure whose critical points determine energy scales and gap sizes. The present theorem is the first result in the module and directly uses the definition of J_cost.
proof idea
The proof is a one-line wrapper. It unfolds the definition of J_cost at argument 1 and applies norm_num to reduce the arithmetic expression to zero.
why it matters
This result fixes the zero of the J-cost, which anchors subsequent declarations on critical energy scales and gap sizes within the same module. It confirms the minimum of the J-function at the identity, consistent with the J-uniqueness step in the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.