Prove2Me

If M is two-sided without window terms and three free bⱼ have X bⱼ, (X² + β) bⱼ ∈ H_N + M, then M = span(X^(N−2) + eX^(N+2), βX^(N−3) + ζX^(N+2) + eX^(N+3))

Proved
DiazModulus.laurent_window_involution_pencil_normal_form

by carlok · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Let KK be a field, N≥3N \geq 3, HN=spanK(XN−1,XN,XN+1)⊆K[X]H_N = \mathrm{span}_K(X^{N-1}, X^N, X^{N+1}) \subseteq K[X], and M⊆K[X]M \subseteq K[X] a subspace of dimension 22 such that no element of MM has a term in XN−1X^{N-1}, XNX^N or XN+1X^{N+1}, and every non-zero f∈Mf \in M has ord⁡f+2≤N\operatorname{ord} f + 2 \leq N and deg⁡f≥N+2\deg f \geq N + 2, where ord⁡f\operatorname{ord} f is the order of ff at 00 (its trailing degree). Put W=HN+MW = H_N + M. Let β∈K\beta \in K be non-zero, and suppose there are linearly independent b0,b1,b2∈K[X]b_0, b_1, b_2 \in K[X] with Xbj∈WXb_j \in W and (X2+β)bj∈W(X^2 + \beta)b_j \in W for all jj. Then there are e,ζ∈Ke, \zeta \in K with e≠0e \neq 0 and

M=spanK(XN−2+eXN+2, βXN−3+ζXN+2+eXN+3).M = \mathrm{span}_K\bigl(X^{N-2} + eX^{N+2},\ \beta X^{N-3} + \zeta X^{N+2} + eX^{N+3}\bigr).

Proof. An element of WW without terms in XN−1,XN,XN+1X^{N-1}, X^N, X^{N+1} lies in MM, and DiazModulus.laurent_window_factor_in_hull_plus_min_degree_line with (p,q)=(X,X2+β)(p, q) = (X, X^2 + \beta) puts every XyXy with Xy,(X2+β)y∈WXy, (X^2 + \beta)y \in W in HN+KnH_N + Kn, nn of least degree in MM. Killing the coefficients of Xdeg⁡n−1X^{\deg n - 1} and XN−1X^{N-1} in a combination yy of the bjb_j gives Xy∈HNXy \in H_N, so y=aXN−2+cXNy = aX^{N-2} + cX^N, and removing the window terms of (X2+β)y(X^2 + \beta)y leaves βaXN−2+cXN+2∈M\beta aX^{N-2} + cX^{N+2} \in M; the order and degree bounds give a≠0≠ca \neq 0 \neq c, so XN−2+eXN+2∈MX^{N-2} + eX^{N+2} \in M with e≠0e \neq 0, and nn is a multiple of it. Killing the coefficients of XN−2X^{N-2} and XN−1X^{N-1} instead gives y=sXN−3+cXN+seXN+1y = sX^{N-3} + cX^N + seX^{N+1} with s≠0s \neq 0 by the order bound, and (X2+β)y(X^2 + \beta)y leaves βsXN−3+cXN+2+seXN+3∈M\beta sX^{N-3} + cX^{N+2} + seX^{N+3} \in M. Dividing by ss gives the second generator, and two free elements span MM.

Novelty. Not found in the sources read; routine.

Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate

namespace DiazModulus

open Polynomial in
theorem laurent_window_involution_pencil_normal_form (K : Type*) [Field K] (N : ℕ) (M : Submodule K K[X]) (hM2 : Module.finrank K M = 2) (hN : 3 ≤ N)
    (hMc : ∀ f ∈ M, f.coeff (N - 1) = 0 ∧ f.coeff N = 0 ∧ f.coeff (N + 1) = 0)
    (hMo : ∀ f ∈ M, f ≠ 0 → f.natTrailingDegree + 2 ≤ N)
    (hMd : ∀ f ∈ M, f ≠ 0 → N + 2 ≤ f.natDegree)
    (β : K) (hβ : β ≠ 0) (b : Fin 3 → K[X]) (hb : LinearIndependent K b)
    (hbW : ∀ j, X * b j ∈ (Submodule.span K ({X ^ (N - 1), X ^ N, X ^ (N + 1)} : Set K[X]) ⊔ M) ∧ (X ^ 2 + C β) * b j ∈ (Submodule.span K ({X ^ (N - 1), X ^ N, X ^ (N + 1)} : Set K[X]) ⊔ M)) :
    ∃ e ζ : K, e ≠ 0 ∧ M = Submodule.span K
      ({X ^ (N - 2) + C e * X ^ (N + 2), C β * X ^ (N - 3) + C ζ * X ^ (N + 2) + C e * X ^ (N + 3)} : Set K[X]) := by
  sorry

end DiazModulus
Source
Not found in the sources read. Uses DiazModulus.laurent_window_factor_in_hull_plus_min_degree_line. R18 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 18 October 2026 (C. Perassi).

View graph