cooper_pair_cost_zero
plain-language theorem explainer
For any positive real x the J-cost of the paired state x times its inverse equals zero. Researchers deriving persistence in coherent recognition structures cite this to obtain a zero-cost reference without presupposing an identity event at x=1. The term proof reduces the argument via multiplicative cancellation then invokes the unit-cost lemma.
Claim. For every real number $x>0$, the J-cost of the state $x x^{-1}$ equals zero.
background
The Observer-Forcing module develops seven steps from coherent recognition to an observer. A recognition event is any positive state with well-defined non-negative J-cost; the explicit form is $J(x)=(x-1)^2/(2x)$. The lemma Jcost_unit0 states that Jcost 1 equals zero. Cooper pairing supplies a zero-cost reference frame even when no event sits directly at the identity tick, as required for a persistent comparison structure across multiple events.
proof idea
The term-mode proof applies the rewrite rule mul_inv_cancel₀ under the hypothesis 0<x to reduce the argument x*x^{-1} to 1, then invokes the lemma Jcost_unit0 to obtain the zero result.
why it matters
This realizes step 6 of the module argument: cooper pairing constructs a persistent reference. It is used directly by the downstream theorem cooper_pairing_yields_persistent to exhibit an explicit persistent recognition event from any positive starting state. In the Recognition framework the result supplies the structural origin of persistence, completing the path from non-trivial coherent recognition to an observer without external posits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.