sigma_nonzero_has_cost
plain-language theorem explainer
Any nonzero sigma incurs strictly positive J-cost under the Recognition cost function. Researchers enforcing coherence limits in superhuman systems cite this to show that deviation from the fixed point cannot be cost-free. The proof is a one-line wrapper that invokes the general positivity lemma for J-cost on positive reals unequal to one.
Claim. For every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $0 < Jcost(x)$.
background
The Safety Interlock module shows that the Gap-45 uncomputability barrier together with sigma-conservation produces a fundamental safety constraint on high-coherence states. J-cost is the deviation measure derived from the recognition composition law, positive away from the fixed point at one; its explicit form is obtained by rewriting as a square over a positive denominator. This theorem appears among the module's core proved results alongside gap45_coprime, sigma_zero_optimal, and weaponization_structurally_impossible.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one (from the Cost module and its JcostCore and LocalCache siblings) directly to the supplied hypotheses on x.
why it matters
The declaration is one of the explicitly listed key results in the Safety Interlock module, closing the argument that nonzero sigma carries unavoidable cost and thereby supporting sigma_zero_optimal (J(1) = 0) and power_ethics_same_axis (higher coherence requires lower sigma). It aligns with the J-uniqueness fixed point and the optimality of the sigma = 0 axis in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.