# A Galois-Theoretic and Frobenius-Descent Viewpoint on a Polynomial Composition Law

Lean formalization for `A Galois-Theoretic and Frobenius-Descent Viewpoint on a Polynomial Composition Law`.

The file verifies the separated composition criterion, the separable generic-fiber argument, Frobenius descent steps, the symmetric/cubic specialization, and the square-root functional-equation proposition.

It is checked with Lean 4.30.0-rc2 and mathlib v4.30.0-rc2.

```powershell
lake exe cache get GaloisFrobeniusCompositionLaw.lean
lake build
```