OAI/NumberTheory/Ostmann/Construction/HistoryCoprimalityRemoval.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_dvd_cleared_iff line 11
2. theorem OAI.Ostmann.zero_cleared_history_support line 18

   Source documentation

   The zero-polynomial branch has empty valid support, including when the reconstructed integer is represented by a cleared numerator.

   theorem zero_cleared_history_support {σ : Type*} (P : MvPolynomial σ ℤ)
       (i : σ) (hP : zeroHistoryVariable i P = 0) (x : σ → ℤ)
       (p : ℕ) (hp : p.Prime) (hxi : x i = p) (d y : ℤ)
       (hN : MvPolynomial.eval₂Hom (RingHom.id ℤ) x P = d * y)
       (hd : ¬p ∣ d.natAbs) : ¬p.Coprime y.natAbs := by
   …

   Mentions: OAI.Ostmann.zeroHistoryVariable

3. theorem OAI.Ostmann.history_coprimality_removal line 30

   Source documentation

   A union bound for the complete finite list of numerator checks. These are the original independent prime priors; no conditioning on history support is introduced.

   theorem history_coprimality_removal {A I : Type*} [Fintype A] [Nonempty A] [Fintype I]
       {n : ℕ} (prime : A → ℕ) (hpInj : Function.Injective prime)
       (hprime : ∀ a, (prime a).Prime)
       (N : I → MvPolynomial (Fin (n + 1)) ℤ) (coord : I → Fin (n + 1))
       (hN : ∀ j, zeroHistoryVariable (coord j) (N j) ≠ 0)
       (μ : Fin (n + 1) → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
       (hmass : ∀ i, ∑ a, μ i a = 1)
       (α V : ℝ) (β H : I → ℝ) (hα : 0 ≤ α) (hβ : ∀ j, 0 ≤ β j)
       (hV : 0 < V) (hH : ∀ j, 1 ≤ H j)
       (hmax : ∀ i a, μ i a ≤ α) (hpmax : ∀ j a, μ (coord j) a ≤ β j)
       (hsize : ∀ a, V ≤ Real.log (prime a : ℝ))
       (hvalue : ∀ j x, |(integerTestValue (fun a => (prime a : ℤ))
   …

   Mentions: OAI.Ostmann.zeroHistoryVariable, OAI.Ostmann.integerTestValue