consistency_defines_composition
plain-language theorem explainer
consistency_defines_composition establishes that the J-cost function satisfies multiplicative consistency, so there exists a combiner P with J(xy) + J(x/y) = P(J(x), J(y)) for positive x, y. Researchers deriving the inevitability of the Recognition Composition Law cite it to close the consistency requirement in the minimal foundation. The proof is a term-mode construction that supplies the explicit quadratic combiner and invokes the d'Alembert identity J_computes_P.
Claim. The cost function $J$ satisfies multiplicative consistency: there exists a combiner $P : ℝ → ℝ → ℝ$ such that $J(xy) + J(x/y) = P(J(x), J(y))$ for all positive real numbers $x, y$.
background
In the Ultimate Inevitability module the foundation reduces to three primitives: symmetry ($F(x) = F(1/x)$), normalization ($F(1) = 0$), and multiplicative consistency ($F(xy) + F(x/y) = P(F(x), F(y))$ for some combiner $P$). The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ that meets these plus smoothness and calibration. The upstream theorem J_computes_P supplies the concrete identity $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$ for positive $x, y$.
proof idea
The proof is a term-mode construction. It exhibits the combiner as the map $(u, v) ↦ 2uv + 2u + 2v$ and then applies the theorem J_computes_P directly to the pair $x, y$ under the positivity hypotheses to verify the equality for J-cost.
why it matters
The result completes the minimal statement that any symmetric normalized consistent cost function is J with combiner the RCL. It supports the module claim that the RCL is not an assumption but what comparison IS, closing the forcing chain at J-uniqueness and the eight-tick octave. The declaration therefore anchors the inevitability argument that Recognition Science has no weaker foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.