taylorWithinEval_succ_real
plain-language theorem explainer
The lemma supplies the recursive relation that advances the Taylor-within-eval polynomial of a real-valued map H from order n to order n+1, adding the explicit next term built from the (n+1)th iterated derivative at the expansion point. Workers on the T5 cost-uniqueness argument cite it when they need concrete low-order expansions to match coefficients against the d'Alembert form of the Recognition Composition Law. The proof is a one-line wrapper that calls the general Mathlib taylorWithinEval_succ lemma and simplifies the scalar-multiplication
Claim. For a function $H : ℝ → ℝ$, a natural number $n$, and points $x_0, x ∈ ℝ$, let $t_k$ denote the Taylor polynomial of degree $k$ for $H$ centered at $x_0$ over the whole real line. Then $t_{n+1}(x) = t_n(x) + [(x - x_0)^{n+1} / (n+1)!] · H^{(n+1)}(x_0)$, where the derivative is the iterated derivative within the full domain.
background
The declaration sits inside the module of functional-equation helpers written for the T5 step of the forcing chain. In that module the auxiliary map H is introduced by the reparametrization H(t) = G(t) + 1, where G is the original cost function; the upstream algebra layer supplies the concrete identification H(x) = J(x) + 1 = ½(x + x^{-1}), which converts the Recognition Composition Law into the classical d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Taylor expansions of H are therefore the natural device for extracting coefficient conditions that enforce this identity. The general recursive relation for such expansions is imported from Mathlib.Analysis.Calculus.Taylor.
proof idea
The proof is a one-line wrapper. It applies the general lemma taylorWithinEval_succ (H n Set.univ x₀ x) and then uses simpa with the rewrite smul_eq_mul to replace the scalar multiplication by ordinary multiplication.
why it matters
The lemma is the inductive engine that produces the explicit first- and second-order Taylor polynomials used by the sibling results taylorWithinEval_one_univ and taylorWithinEval_two_univ. Those polynomials are the concrete objects against which the d'Alembert identity is checked at low orders, thereby supporting the uniqueness claim for the J-cost function at T5. In the larger Recognition Science picture the step contributes to the derivation of J(x) = cosh(log x) - 1 as the unique solution that also satisfies the self-similar fixed-point condition at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.