A177970: formalize the Chebyshev root-sign bridge for consecutive proper position

[PerAlexandersson]

Goal

The A177970 proof client already has a checked native-to-model identity, exact degree,
splitness, and nonvanishing. The two remaining declarations are consecutive
Interlaces and forward Prec.

The smallest exact certificate needed from the model backend is:

theorem A177970Model_eval_mul_derivative_neg
    (d : ℕ) (hd : 2 ≤ d) {r : ℝ}
    (hr : (A177970Model d).IsRoot r) :
    (A177970Model (d + 1)).eval r *
      (A177970Model d).derivative.eval r < 0

Together with the existing facts

• A177970Model_splits,
• A177970Model_natDegree,
• A177970Model_leadingCoeff, and
• derivative_interlaces plus prec_of_interlaces_eval_mul_neg_succ,

this gives model Prec directly; the checked identity
A177970 n = A177970Model (n + 2) then closes both public A177970 targets.

Mathematical proof packet

The complete all-rank argument is in
sqrt-of-2/real-rooted-oeis PR #279,
commit b226a08e, in
A177970-model-interlacing-proof-2026-08-24.md.

For

M_d(t) = (2d+1) E_d(t) - 2d G_d(t)
K_d(x) = 2^(-d) (1+x)^d M_d((x-1)/(x+1)),

it proves

K_d(x) = (2d+1) T_d(x) - 2d R_d(x),
R_d(x) = ((1+x)/2)^(d+1) - (-1)^(d+1) ((1-x)/2)^(d+1).

The current tangent-grid signs place one simple root of K_d in every
Chebyshev slot. At a root of K_d, identities for T_(d+1) and R_(d+1)
give the exact evaluation

K_(d+1)(x) = -(1/d) [
  x T_d(x) + (1-x^2) ((2d+3) T_d'(x) + d R_d'(x))].

Even positive slots are immediate. In odd positive slots, the note proves the
uniform dominance inequality

(1-x^2)(2d+3)|T_d'(x)|
  > x T_d(x) + (1-x^2)d R_d'(x)

by setting x = cos φ, y = sqrt d * φ, and reducing to

(4/pi)y > 1/d + (1+1/d)y^2 exp(-y^2/4).

Central and negative roots then follow by parity. This is exactly the root-sign
certificate above.

Lean-ready decomposition

1. Define the Cayley/Möbius transform locally and prove the displayed formula
   for K_d from A177970Model.

2. Upgrade A177970Model_grid_sign and the exact degree to a root-slot lemma:
   every model root has a unique Chebyshev slot, and all roots are simple.

3. Prove the two first-order identities and the root evaluation formula.
   Mathlib already has Polynomial.Chebyshev.T_real_cos,
   T_derivative_eq_U, and
   one_sub_X_sq_mul_derivative_T_eq_poly_in_T.

4. Formalize the odd-slot scalar estimate. Existing inputs include
   Real.mul_le_sin, Real.lt_tan,
   Real.mul_exp_neg_le_exp_neg_one, Real.exp_neg_one_lt_d9, and numerical
   bounds for pi. One missing upstream-shaped convenience lemma is

   theorem Real.cos_le_exp_neg_sq_div_two
       (hx : |x| ≤ Real.pi / 2) :
       Real.cos x ≤ Real.exp (-(x ^ 2) / 2)

   with proof by applying Real.lt_tan to the derivative of
   log (cos x) + x^2/2 on [0, pi/2) and using evenness.

5. Use parity for the remaining slots, obtain
   A177970Model_eval_mul_derivative_neg, and discharge Prec through the
   existing Ma--Wang constructor.

Formalization boundary

This is not a missing recurrence normalization or a finite-rank problem. The
existing splitness proof consumes tangent-grid sign changes but does not expose
root localization or simplicity. The remaining work therefore includes a new
root-enumeration layer and the uniform analytic odd-slot estimate; bounded
Wronskian searches do not produce a positive coefficient or Bernstein-basis
certificate that would bypass it. This is disproportionate for a generated
one-file client proof and should be implemented in a separate, non-overlapping
backend lane. No axiom, new sorry, or conditional statement scaffold should
be introduced in the client meanwhile.

Current proof surfaces:

• A177970 client
• A177970 model backend