Good primes for edges (round six, `good_edges`)
ProvedIntMul.Kappa.R6.Bit.NB.good_edgesGood primes for edges. Finitely many edges with rational Bruhat data (EdgeQ) are
admissible mod every power of every large prime.
The following holds (Lean statement, in the scope of module Solutions.R6BitNBPrime):
theorem IntMul.Kappa.R6.Bit.NB.good_edges {m : ℕ} (E : Finset (Edge m))
(hE : ∀ e ∈ E, ∃ q : Matrix (Fin m) (Fin m) ℚ, EdgeQ e q) :
∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∀ f : ℕ, ∀ e ∈ E, EdgeOK (q ^ f) e
Context. Round six, bit network: good primes
Finitely many rationals have denominators coprime to every power of every prime q > q₀, and the
nonzero ones are units mod q ^ f. Consequently a finite set of edges with EdgeQ data
is EdgeOK (q ^ f) for all large primes q and all f.
Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs4 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Bit IntMul.Kappa.R6.Bit.NB open Matrix Finset AModelFac
theorem IntMul.Kappa.R6.Bit.NB.good_edges {m : ℕ} (E : Finset (Edge m))
(hE : ∀ e ∈ E, ∃ q : Matrix (Fin m) (Fin m) ℚ, EdgeQ e q) :
∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∀ f : ℕ, ∀ e ∈ E, EdgeOK (q ^ f) e := by sorry