Add certified Galois groups (degree-6 A₄×C₂ / 6T6) via CertifyingInvariantsNF

[CBirkbeck]

What this adds

Brings the Galois-group certification library into LeanBridge, linking LMFDB Galois-group data (nTk labels) to formal Lean proofs. The library is consumed as a lake dependency (IdealArithmetic, from CBirkbeck/CertifyingInvariantsNF@galois-v431-bump), and LeanBridge/Galois.lean re-exports the headline result:

Gal(x⁶ − 5x⁴ − 50x² + 125 / ℚ) ≅ A₄ × C₂ — the transitive group 6T6, order 24.

theorem LeanBridge.Galois.galoisGroup_degSix_isA4timesC2 :
    Nonempty ((f.map (Int.castRingHom ℚ)).Gal ≃*
      alternatingGroup (Fin 4) × Multiplicative (ZMod 2))

theorem LeanBridge.Galois.galoisGroup_degSix_card :
    Nat.card (f.map (Int.castRingHom ℚ)).Gal = 24

The underlying library (available via the dependency)

Reusable, general machinery (all sorry-free, headline results axiom-clean):

• Dedekind's theorem — the cycle type of an arithmetic Frobenius on the roots of f equals the multiset of factor degrees of f mod p, packaged as a user-facing FrobeniusCycleTypeCertificate.
• The discriminant square test — the Galois action lands in Aₙ iff disc is a square (K. Conrad, Thm 4.7).
• Cubic determination — a monic irreducible cubic over ℚ has group A₃ (order 3) or S₃ (order 6) by whether disc is a square.
• Even-polynomial block-sign analysis and the abstract C₂³ ⋊ C₃ ≅ A₄ × C₂ (threeBlockIso), which combine to certify the degree-6 example.

How the example is certified

f = g(X²) with g = Y³ − 5Y² − 50Y + 125 (cyclic cubic ⇒ Gal g ≅ C₃). |Gal f| = |Gal g|·|K| where K is the ±-block kernel; the p = 13 certificate f mod 13 = (X+2)(X+5)(X−5)(X−2)(X²−2) gives one block-transposition, the C₃ symmetry spreads it to K ≅ C₂³ (so |Gal f| = 3·8 = 24), and threeBlockIso identifies Gal f ≅ A₄ × C₂.

Build / provenance notes

• The dependency was ported from Lean v4.30.0-rc1 / mathlib 2ee41a03 to v4.31.0 / fabf563a (LeanBridge's revision) so it compiles on a matching mathlib; no theorem statement changed in the port.
• lake build is green (2620 jobs). The dependency currently points at CBirkbeck/CertifyingInvariantsNF@galois-v431-bump — repoint it if the library moves upstream.

🤖 Generated with Claude Code