Reconstruction of an actual IV.3 k₁ section

The six-key and the five fixed coordinates (r',n₁,n₂,s',h) recover the original extracted tuple, not merely its phase. Canonicality below is expressed by prime support and coprimality, without an extraction oracle.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionDeltaPrime (K : WExtractedKey) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2 / K.2

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionData (K : WExtractedKey) (r n₁ n₂ s k : ℕ) : WGCDData

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionData K r n₁ n₂ s k = { d := K.1.1, d₁ := K.1.2.1, δ := K.1.2.2.1, δ₁ := K.1.2.2.2.1, δ₂ := K.1.2.2.2.2, k₁ := k, k₂ := r * s, n₁ := n₁, n₂ := n₂ }

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple (K : WExtractedKey) (r n₁ n₂ s : ℕ) (h : ℤ) (k : ℕ) : WExtractedTuple × ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple K r n₁ n₂ s h k = ((((K.2, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionDeltaPrime K), r, s), K.1.2.2.1 * K.1.2.2.2.1 * k, K.1.1 * K.1.2.1 * n₁, K.1.1 * n₂), h)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedCanonical (K : WExtractedKey) (r n₁ n₂ s : ℕ) : Prop

All canonical restrictions independent of the varying first modulus. The remaining canonical restrictions are just two coprimalities on k.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedCanonical K r n₁ n₂ s = (0 < K.1.1 ∧ 0 < K.1.2.1 ∧ 0 < K.1.2.2.1 ∧ 0 < K.1.2.2.2.1 ∧ 0 < K.1.2.2.2.2 ∧ 0 < r ∧ 0 < s ∧ 0 < n₁ ∧ 0 < n₂ ∧ (∀ (p : ℕ), Nat.Prime p → p ∣ K.1.2.1 → p ∣ K.1.1) ∧ (∀ (p : ℕ), Nat.Prime p → p ∣ K.1.2.2.2.1 → p ∣ K.1.2.2.1) ∧ (∀ (p : ℕ), Nat.Prime p → p ∣ K.1.2.2.2.2 → p ∣ K.1.2.2.1) ∧ n₁.Coprime K.1.1 ∧ (r * s).Coprime K.1.2.2.1 ∧ (K.1.2.1 * n₁).Coprime n₂ ∧ K.1.2.2.2.1.Coprime (K.1.2.2.2.2 * (r * s)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionData_valid {K : WExtractedKey} {r n₁ n₂ s k : ℕ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hk : 0 < k) (hkδ : k.Coprime K.1.2.2.1) (hkr : k.Coprime (K.1.2.2.2.2 * (r * s))) : (wKSectionData K r n₁ n₂ s k).Valid (K.1.2.2.1 * K.1.2.2.2.1 * k) (K.1.2.2.1 * K.1.2.2.2.2 * (r * s)) (K.1.1 * K.1.2.1 * n₁) (K.1.1 * n₂)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_original {K : WExtractedKey} (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) (r n₁ n₂ s k : ℕ) (h : ℤ) : wExtractedOriginal (wKSectionTuple K r n₁ n₂ s h k).1 = (wKSectionData K r n₁ n₂ s k).original

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_canonical {K : WExtractedKey} {r n₁ n₂ s k : ℕ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hk : 0 < k) (hkδ : k.Coprime K.1.2.2.1) (hkr : k.Coprime (K.1.2.2.2.2 * (r * s))) (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) (h : ℤ) : wGCDTuple (wExtractedOriginal (wKSectionTuple K r n₁ n₂ s h k).1) = wKSectionData K r n₁ n₂ s k

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_kSection_reconstruct {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : wKSectionTuple K t.1.1.2.1 (wGCDTuple (wExtractedOriginal t.1)).n₁ (wGCDTuple (wExtractedOriginal t.1)).n₂ t.1.1.2.2 t.2 (wGCDTuple (wExtractedOriginal t.1)).k₁ = t

Actual key-fiber membership gives exact reconstruction, including the first beta coordinate that does not occur in the analytic five-grid.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_kSection_injective {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t u : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (hu : u ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (hr : t.1.1.2.1 = u.1.1.2.1) (hn₁ : (wGCDTuple (wExtractedOriginal t.1)).n₁ = (wGCDTuple (wExtractedOriginal u.1)).n₁) (hn₂ : (wGCDTuple (wExtractedOriginal t.1)).n₂ = (wGCDTuple (wExtractedOriginal u.1)).n₂) (hs : t.1.1.2.2 = u.1.1.2.2) (hh : t.2 = u.2) (hk : (wGCDTuple (wExtractedOriginal t.1)).k₁ = (wGCDTuple (wExtractedOriginal u.1)).k₁) : t = u

Equal fixed section coordinates and equal k₁ force equality of original tuples. There is no loss of multiplicity in the subsequent sum.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_kSection_data {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : wGCDTuple (wExtractedOriginal t.1) = wKSectionData K t.1.1.2.1 (wGCDTuple (wExtractedOriginal t.1)).n₁ (wGCDTuple (wExtractedOriginal t.1)).n₂ t.1.1.2.2 (wGCDTuple (wExtractedOriginal t.1)).k₁

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_kSection_arithmetic {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : have v := wGCDTuple (wExtractedOriginal t.1); wKSectionFixedCanonical K t.1.1.2.1 v.n₁ v.n₂ t.1.1.2.2 ∧ 0 < v.k₁ ∧ v.k₁.Coprime K.1.2.2.1 ∧ v.k₁.Coprime (K.1.2.2.2.2 * (t.1.1.2.1 * t.1.1.2.2)) ∧ 0 < K.2 ∧ 0 < wKSectionDeltaPrime K ∧ K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2

The canonical constraints are consequences of real membership. This converse is needed for equality of carriers, rather than an inclusion.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_canonical_of_mem {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {r n₁ n₂ s k : ℕ} {h : ℤ} (hd : 0 < K.1.1) (hd₁ : 0 < K.1.2.1) (hδ : 0 < K.1.2.2.1) (hδ₁ : 0 < K.1.2.2.2.1) (ht : wKSectionTuple K r n₁ n₂ s h k ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : wGCDTuple (wExtractedOriginal (wKSectionTuple K r n₁ n₂ s h k).1) = wKSectionData K r n₁ n₂ s k

Even before assuming the variable coprimalities, actual membership forces the reconstructed coordinates to be the canonical ones.