Theorem 4.1 — two conjugate times per Maxwell cell

Does the statement hold: Away from K = 2E, every phase has exactly 2N conjugate times before the end of the N-th Maxwell cell: two per cell, none before the first.

Away from K = 2E, every phase has exactly 2N conjugate times before the end of the N-th Maxwell cell: two per cell, none before the first. Prediction: Lean accepts JacobiFull.roots_ncard using only the standard axioms (no sorry).

Formalised in Lean 4 + Mathlib; #print axioms JacobiFull.roots_ncard after lake build.

Kernel-checked: JacobiFull.roots_ncard compiles and depends only on propext, Classical.choice and Quot.sound.

Excludes the degenerate modulus K = 2E; the excluded-domain arguments of the manuscript are still open.

• JacobiFull.roots_ncard

  Away from K = 2E, every phase has exactly 2N conjugate times before the end of the N-th Maxwell cell: two per cell, none before the first.

  Re-verify