combiner_symmetric
plain-language theorem explainer
Symmetry of the combiner P follows from reciprocal symmetry of the cost function J, surjectivity of J onto the reals, and the defining relation J(xy) + J(x/y) = P(Jx, Jy). Researchers deriving the Recognition Composition Law from ledger axioms cite this as an intermediate step toward factorization. The argument lifts arbitrary u and v to positive preimages x and y, applies the composition law in both orders, and equates the expressions via multiplication commutativity together with J-symmetry on the reciprocal term.
Claim. Let $J : (0,∞) → ℝ$ satisfy $J(x) = J(x^{-1})$ for all $x > 0$. Let $P : ℝ → ℝ → ℝ$ satisfy $J(xy) + J(x/y) = P(J(x), J(y))$ for all $x,y > 0$. If the image of $J$ is all of ℝ, then $P(u,v) = P(v,u)$ for all real $u,v$.
background
The module derives the factorization property, and hence the Recognition Composition Law, from contextual substitutivity and regrouping invariance on a zero-parameter comparison ledger. The function J is the cost function on positive reals; the hypothesis hSym encodes its reciprocal symmetry, while hComp defines the combiner P that adds costs under multiplication and division. Surjectivity of J ensures every real value arises as a cost. The upstream result PrimitiveDistinction.from reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
Tactic-mode proof. Introduce arbitrary u and v. Obtain positive preimages x and y from the surjectivity hypothesis. Apply the composition law once in each order. Rewrite using the images under J. Invoke commutativity of multiplication on the product term. Apply the symmetry hypothesis to the ratio term after field simplification. Close the resulting equality by linear arithmetic.
why it matters
The result is invoked by ledger_forces_regrouping to obtain the full regrouping-invariance package from a zero-parameter ledger. It supplies the symmetry step required before gate_forces_rcl can deliver the RCL polynomial. In the framework it bridges T5 J-uniqueness to the composition law that forces the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.