P_at_zero_right
plain-language theorem explainer
Given F with F(1)=0 and reciprocal symmetry on positives together with any P satisfying the multiplicative consistency F(xy)+F(x/y)=P(F(x),F(y)), the identity P(0,F(y))=2F(y) holds for y>0. Workers deriving the unconditional form of the Recognition Composition Law cite this when fixing the behavior of P on the axes. The term proof reduces the right-hand case to the left-hand case by invoking symmetry of P induced by F.
Claim. Let $F : ℝ → ℝ$ and $P : ℝ → ℝ → ℝ$ satisfy $F(1)=0$, $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 $P(0,F(y))=2F(y)$ for all $y>0$.
background
This declaration belongs to the module establishing the strongest unconditional version of RCL inevitability: both F and P are forced with no prior assumption on P. The local setting requires only normalization at 1, reciprocal symmetry of F, and existence of some P obeying the consistency relation; smoothness and calibration appear only in later steps of the same module. Upstream, P_symmetric_of_F_symmetric shows that reciprocal symmetry of F forces symmetry of P, while the companion P_at_zero_left already gives P(F(x),0)=2F(x) on the range of F.
proof idea
The term proof applies P_symmetric_of_F_symmetric to the arguments (1,y) to obtain P(F(1),F(y))=P(F(y),F(1)). After rewriting F(1)=0 this yields P(0,F(y))=P(F(y),0). It then calls P_at_zero_left on y and rewrites the resulting equality to finish.
why it matters
The result completes the axis values of P inside the full unconditional theorem, enabling the duplication formula and the subsequent ODE that forces F=J. It supports the framework step from the bare consistency equation to the explicit bilinear form P(u,v)=2uv+2u+2v required for the phi-ladder and eight-tick octave. The module doc emphasizes that this version assumes nothing about P, closing a gap left by earlier partial unconditional arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.