P_determined_on_range
plain-language theorem explainer
The theorem shows that any P satisfying the multiplicative consistency J(xy) + J(x/y) = P(J(x), J(y)) for positive x, y must equal the bilinear expression 2uv + 2u + 2v on pairs drawn from the image of J. Researchers deriving the Recognition Composition Law from symmetry and normalization assumptions would cite it to establish that P is computed rather than freely chosen. The proof is a one-line wrapper that reverses the hypothesis and invokes the d'Alembert identity already verified for J.
Claim. Let $J$ be the J-cost function. If $P : (0,∞) × (0,∞) → ℝ$ satisfies $J(xy) + J(x/y) = P(J(x), J(y))$ for all $x,y > 0$, then $P(J(x), J(y)) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$ for all $x,y > 0$.
background
The J-cost function is defined by $J(x) = (x + x^{-1})/2 - 1$ and satisfies the d'Alembert identity $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$ on positive reals. The module establishes unconditional inevitability of the Recognition Composition Law: once F is symmetric, normalized at 1, calibrated by second derivative, and smooth, it is forced to equal J, after which P is computed directly from the functional equation with no further assumptions on P. Upstream, J_computes_P records the identity for J itself.
proof idea
The proof is a one-line wrapper. It introduces positive x and y, rewrites the target equality by inverting the hypothesis hCons, and applies J_computes_P to obtain the explicit bilinear form.
why it matters
P_determined_nonneg invokes this result to extend determination of P to the full non-negative quadrant once surjectivity of J is available. It completes the step showing P is uniquely computed from the functional equation applied to J, supporting the unconditional RCL inevitability and the T5 J-uniqueness landmark in the forcing chain. The module doc-comment notes that this closes the possibility of irregular solutions for P on the range of J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.