J_surjective_nonneg
plain-language theorem explainer
The J-cost function maps positive reals onto all nonnegative reals. Researchers deriving the Recognition Composition Law without assumptions on P cite this to confirm that the pairing function is fully determined on the nonnegative quadrant. The proof splits into the zero case with the explicit point x=1 and the positive case by constructing the positive root of the quadratic x + 1/x = 2v + 2 and verifying the identity by algebraic cancellation.
Claim. For every real number $v$ with $v ≥ 0$ there exists a positive real $x$ such that $J(x) = v$, where $J(x) := (x + x^{-1})/2 - 1$.
background
The Unconditional RCL Inevitability module shows that any function F satisfying symmetry F(x) = F(x^{-1}), normalization F(1) = 0, C² smoothness, and multiplicative consistency with some pairing P must equal the explicit J-cost function. J-cost is defined by Cost.Jcost x = (x + 1/x)/2 - 1 on positive reals and satisfies the Recognition Composition Law with the bilinear form P(u, v) = 2uv + 2u + 2v. The module proves this form is forced by ODE uniqueness once the basic properties of F are granted, with no regularity hypothesis imposed on P itself.
proof idea
The tactic proof opens with by_cases on v = 0. The zero case supplies x = 1 and reduces by simp. For v > 0 it computes the discriminant, proves positivity by ring and mul_pos, defines the positive root x, establishes x > 0 by div_pos and linarith, then shows the quadratic relation x² - (2v + 2)x + 1 = 0 by field_simp and ring_nf. From the quadratic it derives x + x^{-1} = 2v + 2 by linarith and field_simp, after which a short calc block reduces J(x) to v.
why it matters
This result is invoked by P_determined_nonneg to obtain the explicit form of P on [0, ∞)² and thereby by full_inevitability_explicit to close the unconditional forcing argument. It supplies the surjectivity step required for the claim that P is computed rather than postulated once F is fixed to J, aligning with the T5 J-uniqueness landmark and the module's statement that no assumption on P is needed. The construction touches the gap between the functional equation and the explicit bilinear pairing in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.