Evaluating the universal rational functions

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import Mathlib.FieldTheory.RatFunc.AsPolynomial7import SurfaceBlowup.Formula.StateCombinatorics8 9/-!10# Evaluating the universal rational functions11 12The rational function `Expr.rational` of a safe expression evaluates at `q` to the value of the13expression; in particular the monic and projective expressions evaluate correctly at every prime14power.15 16## Main results17 18* `SurfaceBlowup.global_rational_eval`19 20Provenance: `Thm_SurfaceBlowupV2_{expression_rational_eval, global_rational_eval}` (moved from21`Blowup/CurveOrders.lean`).22-/23 24namespace SurfaceBlowup25 26/-- Evaluating the rational function of a safe expression at `q` gives its value at `q`. -/27private theorem expression_rational_eval (x : Expr) (q : ℚ) (hx : x.safe q) :28    RatFunc.eval (RingHom.id ℚ) q x.rational = x.eval q := by29  obtain ⟨hQ, hval⟩ := expression_fraction x q hx30  have hrat : x.rational = algebraMap _ _ x.fraction.1 / algebraMap _ _ x.fraction.2 := rfl31  have hQ0 : x.fraction.2 ≠ 0 := by32    intro h; apply hQ; rw [h]; simp33  have hQ0' : algebraMap (Polynomial ℚ) (RatFunc ℚ) x.fraction.2 ≠ 0 :=34    RatFunc.algebraMap_ne_zero hQ035  have hden : (RatFunc.denom x.rational).eval₂ (RingHom.id ℚ) q ≠ 0 := by36    intro h37    have hd : RatFunc.denom x.rational ∣ x.fraction.2 := by38      rw [hrat]; exact RatFunc.denom_div_dvd _ _39    exact hQ (Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hd h)40  have h2 : x.rational * algebraMap _ _ x.fraction.2 = algebraMap _ _ x.fraction.1 := by41    rw [hrat]; exact div_mul_cancel₀ _ hQ0'42  have h3 := RatFunc.eval_mul (f := RingHom.id ℚ) (a := q) (x := x.rational)43    (y := algebraMap _ _ x.fraction.2) hden44    (by rw [RatFunc.denom_algebraMap]; simp)45  rw [h2] at h346  have eP : RatFunc.eval (RingHom.id ℚ) q (algebraMap _ _ x.fraction.1) = x.fraction.1.eval q := by47    rw [RatFunc.eval_algebraMap]; simp [Polynomial.eval₂_id]48  have eQ : RatFunc.eval (RingHom.id ℚ) q (algebraMap _ _ x.fraction.2) = x.fraction.2.eval q := by49    rw [RatFunc.eval_algebraMap]; simp [Polynomial.eval₂_id]50  rw [eP, eQ] at h351  rw [hval, eq_div_iff hQ]52  exact h3.symm53 54/-- The rational functions of the monic and projective expressions evaluate correctly at55prime powers. -/56theorem global_rational_eval (n : ℕ) (σ : FactorType) :57    ∀ q : ℕ, PrimePower q → RatFunc.eval (RingHom.id ℚ) q (monicExpr n σ).rational =58        (monicExpr n σ).eval q ∧ RatFunc.eval (RingHom.id ℚ) q (projectiveExpr n σ).rational =59        (projectiveExpr n σ).eval q := by60  intro q hq61  have h2 := prime_power_ge_two q hq62  obtain ⟨h1, h3⟩ := global_coefficients_safe n σ63  exact ⟨expression_rational_eval _ _ (h1 q h2),64    expression_rational_eval _ _ (h3 q h2)⟩65 66end SurfaceBlowup