rs_exists_iff_zero_cost
plain-language theorem explainer
For positive reals the J-cost vanishes exactly at unity. Researchers dissolving the simulation hypothesis in Recognition Science cite the equivalence to tie ledger existence to zero deviation from the unit. The proof splits the biconditional, rewrites via the squared cost identity, isolates the squared difference, and concludes by nonnegativity in one direction while invoking the direct unit evaluation in the other.
Claim. For every positive real number $x$, $J(x)=0$ if and only if $x=1$, where $J(x)=(x-1)^2/(2x)$.
background
The module treats the ledger as identical to physical reality, so that any purported external simulation collapses into the same structure. J-cost is the deviation measure given by the squared ratio $J(x)=(x-1)^2/(2x)$ for nonzero $x$, with the special value $J(1)=0$ supplied by direct evaluation. The upstream squared-form lemma converts the original hyperbolic expression into this algebraic shape, while the unit-zero lemma records the vanishing at the fixed point.
proof idea
Constructor splits the biconditional. Forward direction rewrites the hypothesis with the squared-cost lemma, clears the positive denominator by linarith, isolates the squared term, and applies nlinarith on nonnegativity of squares. Reverse direction substitutes the equality and applies the unit-zero lemma.
why it matters
The result supplies IC-004.6, anchoring the claim that RS existence is precisely the zero-cost condition at unity. It feeds the certificate that any universe reproducing RS dynamics must operate over the reals. Within the framework it reinforces the J-uniqueness step and the self-grounded ledger, closing the category error that would otherwise allow an external simulation substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.