P_at_zero_right
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume differentiability or C² regularity of F.
- Does not prove uniqueness of F or of P.
- Applies only for positive y and on the image of F.
- Does not treat zero or negative arguments.
- Does not derive the explicit form of P away from the axes.
formal statement (Lean)
111theorem P_at_zero_right
112 (F : ℝ → ℝ)
113 (P : ℝ → ℝ → ℝ)
114 (hUnit : F 1 = 0)
115 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
116 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
117 ∀ y : ℝ, 0 < y → P 0 (F y) = 2 * F y := by
proof body
Term-mode proof.
118 intro y hy
119 -- Use symmetry of P
120 have hP_symm := P_symmetric_of_F_symmetric F P hSymm hCons 1 y one_pos hy
121 rw [hUnit] at hP_symm
122 have h := P_at_zero_left F P hUnit hCons y hy
123 rw [hP_symm]
124 exact h
125
126/-! ## Part 3: The Duplication Formula -/
127
128/-- Setting x = y gives the duplication formula: F(x²) + F(1) = P(F(x), F(x)) -/