P_symmetric_on_range
plain-language theorem explainer
P_symmetric_on_range shows that the auxiliary function P arising from multiplicative consistency is symmetric on the image of any reciprocal-symmetric F. Researchers deriving the explicit form of the Recognition Composition Law would cite it as the first step that lifts pointwise symmetry to the range before invoking normalization. The proof is a direct one-line wrapper that invokes the pointwise symmetry lemma on the witnessing preimages and substitutes the range values.
Claim. Let $F:ℝ→ℝ$ and $P:ℝ→ℝ→ℝ$ satisfy $F(x)=F(x^{-1})$ for all $x>0$ and $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$. Then for all $u,v$ in the range of $F$ (i.e., $u=F(x)$ and $v=F(y)$ for some $x,y>0$), one has $P(u,v)=P(v,u)$.
background
The module FullUnconditional establishes the strongest form of RCL inevitability: given any $F:ℝ₊→ℝ$ obeying normalization ($F(1)=0$), reciprocal symmetry, $C^2$ smoothness, calibration $G''(0)=1$ with $G(t)=F(e^t)$, and the existence of some $P$ satisfying the multiplicative consistency equation, both $F$ and $P$ are forced to be the J-cost and the bilinear form $2uv+2u+2v$. Normalization is the axiom that the cost vanishes at unity, encoding perfect balance. The upstream lemma P_symmetric_of_F_symmetric already proves symmetry of $P(F(x),F(y))$ directly from the reciprocal symmetry of $F$; the present result merely extends that equality to arbitrary elements of the range.
proof idea
The term-mode proof introduces the range witnesses $x$ and $y$ for $u$ and $v$, applies the pointwise symmetry theorem P_symmetric_of_F_symmetric to obtain $P(F x,F y)=P(F y,F x)$, and rewrites the left-hand sides by the defining equations $F x=u$ and $F y=v$.
why it matters
This lemma supplies the symmetry property of $P$ needed for the subsequent derivation of $P(u,0)=2u$ from normalization inside the same module. It therefore participates in the chain that concludes $P(u,v)=2uv+2u+2v$ without any a-priori assumption on the shape of $P$, completing the full unconditional RCL theorem. In the Recognition Science framework the result supports the forcing of the J-cost (T5) and the eight-tick octave structure (T7) by ensuring the composition law is symmetric before the ODE uniqueness step is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.