taylorWithinEval_two_univ
plain-language theorem explainer
The lemma supplies the explicit quadratic Taylor polynomial for the shifted cost function H at the origin over all reals. Workers proving uniqueness of solutions to the d'Alembert equation for H in the T5 step of the forcing chain would cite this expansion when matching coefficients near zero. The proof reduces the order-2 case to the already-established order-1 case via the successor recurrence for Taylor polynomials and normalizes the second-derivative coefficient by direct algebraic simplification.
Claim. Let $H : ℝ → ℝ$ be the shifted cost function. Then the degree-2 Taylor polynomial of $H$ centered at $0$, evaluated at any $x ∈ ℝ$, satisfies $T_2(H;0)(x) = H(0) + H'(0)·x + H''(0)·x²/2$.
background
The module supplies auxiliary results for the T5 cost-uniqueness argument. Here $H$ is the reparametrization $H(t) = G(t) + 1$, where $G$ satisfies the cosh-type functional identity obtained from the Recognition Composition Law. Upstream, the same $H$ is defined by $H(x) = J(x) + 1 = ½(x + x⁻¹)$, converting the RCL into the standard d'Alembert equation $H(xy) + H(x/y) = 2·H(x)·H(y)$. The Taylor lemmas in this file therefore analyze the local power-series behavior of this $H$ at the identity point.
proof idea
Apply taylorWithinEval_succ_real at order 1 to obtain the recurrence relating the degree-2 polynomial to the degree-1 polynomial plus a quadratic increment involving iteratedDerivWithin 2. Substitute the explicit order-1 formula from taylorWithinEval_one_univ. Identify iteratedDerivWithin 2 H univ 0 with the second derivative by the simplification iteratedDerivWithin_univ and iteratedDeriv_succ. Finally rewrite the coefficient ((2·1!)⁻¹) to 1/2 and collect terms.
why it matters
The result supplies the quadratic term needed to match coefficients in the T5 uniqueness argument for the J-cost functional equation. It sits inside the chain that forces the cosh form (T5) and thereby the self-similar fixed point phi (T6) and the eight-tick octave (T7). No direct downstream citations appear yet, but the lemma closes the local Taylor analysis required before global solution matching on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.