taylorWithinEval_one_univ
plain-language theorem explainer
The lemma states that the order-1 Taylor polynomial of an arbitrary real function H, centered at zero and evaluated over the entire real line, reduces exactly to the constant term H(0) plus the first derivative at zero times the variable x. Analysts constructing the power series solution to the d'Alembert-type equation for the shifted cost H in the T5 uniqueness argument would invoke this step when inducting on the Taylor order. The proof is a direct simplification of the successor Taylor formula at n=0 using iterated derivative identities and
Claim. Let $H : ℝ → ℝ$. Then the first-order Taylor expansion of $H$ within the full real line, centered at 0 and evaluated at $x$, equals $H(0) + H'(0) · x$.
background
This lemma sits in the module of functional-equation helpers for the T5 J-uniqueness proof. The symbol H denotes the shifted cost reparametrization H_F(t) = G_F(t) + 1, where G satisfies the Recognition Composition Law; in the algebra layer the same H is defined by H(x) = J(x) + 1 with J(x) = ½(x + x⁻¹), converting the RCL into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The immediate predecessor lemma taylorWithinEval_succ_real supplies the general recursive step that adds the next iterated-derivative term.
proof idea
The proof calls taylorWithinEval_succ_real at n=0, then uses simp to reduce iteratedDerivWithin_univ and iteratedDeriv_one to the plain derivative, followed by simpa with mul_comm to obtain the target linear form.
why it matters
The result is the base case that feeds taylorWithinEval_two_univ and the subsequent inductive construction of the Taylor series for H. It therefore contributes to the explicit power-series identification of solutions to the functional equation, which is required for the T5 step that forces J(x) = cosh(log x) - 1 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.