P_determined_nonneg
plain-language theorem explainer
The theorem shows that any P satisfying the consistency equation with Jcost on positive reals must equal the bilinear form 2uv + 2u + 2v on the full non-negative quadrant. Recognition Science researchers working on the unconditional form of the Recognition Composition Law cite it to rule out irregular solutions for P. The term-mode proof reduces the non-negative case to the positive range by invoking surjectivity of Jcost.
Claim. Suppose $P : (0,∞) → ℝ$ satisfies $J(xy) + J(x/y) = P(J(x), J(y))$ for all $x,y > 0$, where $J(z) = (z + z^{-1})/2 - 1$. Then $P(u,v) = 2uv + 2u + 2v$ for all $u,v ≥ 0$.
background
The J-cost function is J(x) = (x + x^{-1})/2 - 1, which maps (0,∞) onto [0,∞) and obeys the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The Unconditional module proves that if F : ℝ₊ → ℝ satisfies symmetry F(x) = F(1/x), normalization F(1) = 0, calibration G''(0) = 1 with G(t) = F(exp(t)), and smoothness, then F must coincide with J and the pairing function P in the functional equation is forced to the bilinear expression above. This builds directly on J_surjective_nonneg (J maps onto [0,∞)) and P_determined_on_range (P is fixed on the positive image).
proof idea
The term-mode proof proceeds by reduction to the positive case. For arbitrary u,v ≥ 0 it obtains positive preimages x,y via J_surjective_nonneg such that J(x) = u and J(y) = v. It then applies P_determined_on_range to the pair (x,y) and substitutes the equalities back to obtain the identity on (u,v).
why it matters
This declaration extends the range determination from positive reals to the closed quadrant, completing the unconditional RCL statement. It is invoked directly by rcl_unconditional to obtain the full inevitability theorem on [0,∞)² and feeds into full_unconditional_inevitability. In the framework it closes the mathematician's concern about irregular solutions by showing P is computed from J rather than assumed, consistent with T5 J-uniqueness and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.