perturbed_cost_positive
plain-language theorem explainer
The theorem states that the J-cost is strictly positive for every positive real number away from the fixed point at unity. Researchers deriving the GCIC from the forcing chain cite it to bound excess cost from phase perturbations. The proof is a direct one-line application of the core positivity lemma for Jcost.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. For every real $x > 0$ with $x ≠ 1$, one has $J(x) > 0$.
background
The module derives the Global Co-Identity Constraint from the J-cost forcing chain with no empirical axioms. The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ that vanishes only at the self-similar point $x=1$ and is positive elsewhere for $x>0$; this positivity follows from T5 J-uniqueness in the chain T5 to T8. The upstream lemma Jcost_pos_of_ne_one states exactly that $J(x) > 0$ for $x ≠ 1$ and $x > 0$, proved by rewriting Jcost as a square over a positive denominator.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one x hx hne from the Cost module.
why it matters
This auxiliary result supplies the positivity needed to compare aligned collective cost against the sum of perturbed costs in the GCIC derivation. It directly instantiates the T5 J-uniqueness property inside the paper's forcing chain T5 to T8. No open questions are addressed; the statement is fully proved and closes a basic gap in the phase-alignment arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.