The degenerate split trace cover has no principal syntactic division theorem

At sigma = 1 and d = e = 1, the cleared cover polynomial is the product (y - x) * (x * y - 1). The Kummer tower selects the component x * y = 1. Consequently its evaluation kernel strictly contains the ideal generated by the whole cleared polynomial. This file records that obstruction explicitly: the source-side division statement must assume the nondegeneracy condition sigma != 1.

noncomputable def BGS.Markoff.splitTraceDegenerateKummerComponent {K : Type u_1} [Field K] : MvPolynomial (Fin 2) K

The component selected by the Kummer parametrization when sigma = d = e = 1.

Equations

• BGS.Markoff.splitTraceDegenerateKummerComponent = MvPolynomial.X 0 * MvPolynomial.X 1 - 1

theorem BGS.Markoff.splitTraceDegenerateKummerComponent_syntacticNormalForm_eq_zero {K : Type u_1} [Field K] : splitTracePolynomialSyntacticNormalForm 1 ⋯ 1 1 splitTraceDegenerateKummerComponent_syntacticNormalForm_eq_zero._proof_1 splitTraceDegenerateKummerComponent_syntacticNormalForm_eq_zero._proof_1 splitTraceDegenerateKummerComponent = 0

The Kummer-selected component has zero syntactic normal form.

theorem BGS.Markoff.splitTraceDegenerateKummerComponent_not_mem_coverIdeal {K : Type u_1} [Field K] : splitTraceDegenerateKummerComponent ∉ Ideal.span {splitTraceCoverPolynomial 1 1 1 1}

The Kummer-selected component is not a multiple of the full degenerate cover polynomial. Evaluation at the affine origin separates them.

theorem BGS.Markoff.not_splitTraceSyntacticNormalForm_division_at_degenerateParameter {K : Type u_1} [Field K] : ¬∀ (p : MvPolynomial (Fin 2) K), splitTracePolynomialSyntacticNormalForm 1 ⋯ 1 1 splitTraceDegenerateKummerComponent_syntacticNormalForm_eq_zero._proof_1 splitTraceDegenerateKummerComponent_syntacticNormalForm_eq_zero._proof_1 p = 0 → p ∈ Ideal.span {splitTraceCoverPolynomial 1 1 1 1}

Therefore the source-side division assertion used by the affine injectivity endpoint is false without the paper's nondegeneracy hypothesis sigma != 1.

theorem BGS.Markoff.not_splitTraceAffineToKummerTop_injective_at_degenerateParameter {K : Type u_1} [Field K] : ¬Function.Injective ⇑(splitTraceAffineToKummerTop 1 ⋯ 1 1 splitTraceDegenerateKummerComponent_syntacticNormalForm_eq_zero._proof_1 splitTraceDegenerateKummerComponent_syntacticNormalForm_eq_zero._proof_1 not_splitTraceAffineToKummerTop_injective_at_degenerateParameter._proof_1)

At the degenerate parameter, the affine comparison map itself is not injective: the nonzero class of x * y - 1 maps to zero.