time_reversed_pair_zero_cost
plain-language theorem explainer
The result shows that for positive real x the J-cost of the product x times its inverse is zero. Condensed matter theorists deriving Cooper pair stability from Recognition Science would cite it as the zero-cost anchor for pairing instability. The term proof cancels the product to unity via the inverse property and invokes the unit lemma for J-cost at one.
Claim. Let $J(y) = (y-1)^2/(2y)$ denote the J-cost function. For every real $x > 0$, $J(x · x^{-1}) = 0$.
background
The J-cost function is defined by $J(y) = (y-1)^2/(2y)$ and is nonnegative, vanishing only at unity (from the upstream lemma Jcost_unit0). In this module the BCS treatment models time-reversed electron pairs as ledger ratios x and x^{-1} whose product equals the J-cost minimizer at one. The local setting is the derivation of Cooper instability directly from J-cost submultiplicativity, with the cost of any recognition event identified with its J-cost.
proof idea
The term-mode proof first obtains x ≠ 0 from the positivity hypothesis via ne_of_gt, rewrites the product to 1 by mul_inv_cancel₀, and applies the lemma Jcost_unit0 exactly.
why it matters
This theorem supplies the zero-cost base case for the downstream cooper_criterion and pairing_lowers_cost statements. It realizes the J-cost minimizer at unity as the foundation for the abstract Cooper instability theorem inside the Recognition Science BCS derivation, linking to the multiplicative recognizer cost and observer forcing cost. It closes the base step needed for the universal gap ratio 2Δ/(k_B T_c) ≈ 3.52.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.