@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB10Congruence (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB10Congruence P = Classical.propDecidable P

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductFiber (N : ℕ) (b c : ℝ) (m : ℕ) : Finset (ℕ × ℕ)

The corrected C10 product fibre over a fixed value m = rs.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductFiber N b c m = {rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs = m}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Coeff (N : ℕ) (b c : ℝ) (m : ℕ) : ℕ

The actual finite C10 coefficient α(m) = #{rs ∈ C10 : rs = m}.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Coeff N b c m = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductFiber N b c m).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachC10ProductFiber_iff {N : ℕ} {b c : ℝ} {m : ℕ} {rs : ℕ × ℕ} : rs ∈ goldbachC10ProductFiber N b c m ↔ rs ∈ goldbachC10Pairs N b c ∧ goldbachC10Prod rs = m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod_injOn {N : ℕ} {b c : ℝ} : Set.InjOn goldbachC10Prod ↑(goldbachC10Pairs N b c)

On the corrected C10 carrier, the ordered prime-factor label rs ↦ r*s is injective, even when r = s.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Coeff_le_one {N : ℕ} {b c : ℝ} {m : ℕ} : goldbachC10Coeff N b c m ≤ 1

The literal C10 coefficient α(m) is at most 1.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atom_prod_lt {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachB10Atoms N ε b c) : goldbachC10Prod x.fst * x.snd < N

A genuine labelled B10 atom always satisfies the strict product bound mq < N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atom_output_eq_sub (N : ℕ) (x : (_ : ℕ × ℕ) × ℕ) : goldbachPi10Output N x = N - goldbachC10Prod x.fst * x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atom_prod_add_output {N : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachB10Atoms N ε b c) : goldbachC10Prod x.fst * x.snd + goldbachPi10Output N x = N

For an actual labelled B10 atom, the literal output p = N - mq reconstructs N exactly as mq + p = N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atom_output_dvd_iff_modEq {N d : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (_hd : 1 ≤ d) (hx : x ∈ goldbachB10Atoms N ε b c) : d ∣ goldbachPi10Output N x ↔ goldbachC10Prod x.fst * x.snd ≡ N [MOD d]

On a genuine labelled B10 atom, divisibility of the output p = N - mq is equivalent to the natural-number congruence mq ≡ N (mod d).

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atom_prod_coprime_of_coprime_modulus {N d : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (_hd : 1 ≤ d) (hdN : d.Coprime N) (hx : x ∈ goldbachB10Atoms N ε b c) (hdp : d ∣ goldbachPi10Output N x) : (goldbachC10Prod x.fst).Coprime d

If the actual output p = N - mq is divisible by d and d is coprime to N, then the product label m = rs is automatically coprime to d.

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorResidueCondition (N d : ℕ) (x : (_ : ℕ × ℕ) × ℕ) : Prop

The exact residue-class condition on a divisor fibre of genuine labelled B10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorResidueCondition N d x = ((MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod x.fst).Coprime d ∧ ↑x.snd = ↑N * (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod x.fst))⁻¹)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atom_output_dvd_iff_residueCondition {N d : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hx : x ∈ goldbachB10Atoms N ε b c) : d ∣ goldbachPi10Output N x ↔ goldbachB10DivisorResidueCondition N d x

On the actual divisor fibre with d ≥ 1 and (d, N) = 1, divisibility of the output p = N - mq is equivalent to the precise coprimality-plus-inverse residue condition on the same label ((r,s),q).

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms (N d : ℕ) (ε b c : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

The labelled divisor fibre inside the genuine finite B10 atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms N d ε b c = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Atoms N ε b c | d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10Output N x}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB10DivisorAtoms_iff {N d : ℕ} {ε b c : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB10DivisorAtoms N d ε b c ↔ x ∈ goldbachB10Atoms N ε b c ∧ d ∣ goldbachPi10Output N x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms_eq_residueFilter {N d : ℕ} {ε b c : ℝ} (hd : 1 ≤ d) (hdN : d.Coprime N) : goldbachB10DivisorAtoms N d ε b c = Finset.filter (goldbachB10DivisorResidueCondition N d) (goldbachB10Atoms N ε b c)

On each labelled atom, the divisor filter can be replaced exactly by the coprimality-plus-inverse residue condition from goldbachB10Atom_output_dvd_iff_residueCondition.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10DivisorAtoms_card_eq_residueFilter_card {N d : ℕ} {ε b c : ℝ} (hd : 1 ≤ d) (hdN : d.Coprime N) : (goldbachB10DivisorAtoms N d ε b c).card = (Finset.filter (goldbachB10DivisorResidueCondition N d) (goldbachB10Atoms N ε b c)).card