Jcost_eq_zero_iff
plain-language theorem explainer
J(x) vanishes exactly at x equals one for positive reals. Researchers tracking persistent states or zero-cost ledger entries cite the equivalence to isolate unity. The term proof splits the biconditional, derives a contradiction from positivity away from one, and substitutes the unit evaluation.
Claim. For all real $x > 0$, $J(x) = 0$ if and only if $x = 1$, where $J(x) := (x + x^{-1})/2 - 1$.
background
The J-cost is the function $J(x) := (x + x^{-1})/2 - 1$ introduced in the Cost module to quantify deviation from unity in recognition and ledger settings. The module develops algebraic identities for this cost ahead of its use in forcing chains and observer structures.
proof idea
Constructor splits the biconditional. The forward direction assumes $Jcost x = 0$, supposes $x ≠ 1$, and invokes Jcost_pos_of_ne_one to reach a contradiction with the strict positivity statement. The reverse direction rewrites the hypothesis $x = 1$ and applies Jcost_unit0.
why it matters
The equivalence pins the unique minimum of J-cost and feeds Jcost_zero_iff_one together with persistent_state_unique and entry_cost_zero_iff_unity. It supplies the algebraic content of T5 J-uniqueness in the forcing chain, where unity is the fixed point for coherent recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.