P_at_zero_left
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume symmetry or smoothness of F.
- Does not determine P for nonzero second argument.
- Does not extend the domain to non-positive reals.
- Does not prove existence of any F satisfying the premises.
formal statement (Lean)
96theorem P_at_zero_left
97 (F : ℝ → ℝ)
98 (P : ℝ → ℝ → ℝ)
99 (hUnit : F 1 = 0)
100 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
101 ∀ x : ℝ, 0 < x → P (F x) 0 = 2 * F x := by
proof body
Term-mode proof.
102 intro x hx
103 -- Set y = 1 in the consistency equation
104 have h := hCons x 1 hx one_pos
105 simp only [mul_one, div_one] at h
106 rw [hUnit] at h
107 -- h : F x + F x = P (F x) 0
108 linarith
109
110/-- Similarly, P(0, v) = 2v on the range of F. -/