P_at_zero_left
plain-language theorem explainer
This result shows that if F satisfies F(1)=0 and obeys the multiplicative consistency relation with some P, then P(u,0)=2u for every u in the image of F. Researchers deriving the unconditional form of the Recognition Composition Law cite it to fix the zero-normalization of P before the ODE step. The proof is a direct substitution of y=1 into the consistency equation followed by algebraic simplification with mul_one and linear arithmetic.
Claim. Let $F : (0,∞) → ℝ$ and $P : ℝ → ℝ → ℝ$. If $F(1)=0$ and $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$, then $P(F(x),0)=2F(x)$ for all $x>0$.
background
The Full Unconditional module derives both F and P without assuming the form of P, given only normalization F(1)=0, reciprocal symmetry, C² smoothness, calibration G''(0)=1, and the existence of some P satisfying the consistency equation. This lemma isolates the consequence of normalization at the zero argument of P. It draws on the arithmetic identity mul_one (n * 1 = n) and on the consistency equation imported from the Unconditional and Inevitability submodules.
proof idea
The proof is a one-line wrapper that applies the consistency hypothesis at y=1, rewrites using mul_one and div_one, substitutes the unit condition F(1)=0, and concludes by linear arithmetic.
why it matters
This lemma supplies the left-zero normalization for P in the chain that forces both F and P to their explicit J and RCL forms. It is invoked directly by the companion result P_at_zero_right, which together enable the ODE uniqueness argument for G. In the Recognition framework it closes the normalization step toward T5 J-uniqueness and the subsequent eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.