ArithmeticCandidateKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The original candidate weights and the masked residue kernel

def OAI.JointDickman.candidateArithmeticQuotient line 10
theorem OAI.JointDickman.candidateArithmeticQuotient_equation line 17
Source documentation
Both endpoint divisibilities reconstruct the affine quotient, without any counting-scale cutoff or squarefree-site assumption.
```
theorem candidateArithmeticQuotient_equation {B L T H M u : ℕ} {τ C : ℝ}
    (hT : T ≤ auxiliaryCutoff B) {e : BlockCandidateIndex M}
    (he : e ∈ blockCandidates B L T H M τ C
      (fun i => coefficientPrimeSet B (u+(i.val+1)))) :
    candidateHigh e*candidateLow e*candidateArithmeticQuotient u e+candidateLow e =
      candidateQuotient e*(u+(e.1.1.val+1)) := by
…
```
Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.blockCandidates, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateArithmeticQuotient, OAI.JointDickman.candidateQuotient
theorem OAI.JointDickman.arithmeticCandidatePrimeFamily_transpose line 58
def OAI.JointDickman.actualCandidateKernel line 73

theorem OAI.JointDickman.actualCandidateKernel_eq_masked line 83

Source documentation

Pointwise identification of the arithmetic kernel with the masked model outside the three explicitly bounded exceptional events.

theorem actualCandidateKernel_eq_masked {B L T H M u : ℕ} {τ C : ℝ}
    (hT : T ≤ auxiliaryCutoff B) (χ : BlockCandidateIndex M → ℝ)
    (hforce : ∀ e ∈ blockCandidates B L T H M τ C
      (fun i => coefficientPrimeSet B (u+(i.val+1))),
      ¬ CandidateForcedWitness B e (fun i => coefficientPrimeSet B (u+(i.val+1))))
    (hactual : ¬ ArithmeticCoefficientHit B
      (blockCandidates B L T H M τ C (fun i => coefficientPrimeSet B (u+(i.val+1))))
      (candidateArithmeticQuotient u))
    (hmasked : ¬ MaskedCoefficientEvent
      (blockCandidates B L T H M τ C (fun i => coefficientPrimeSet B (u+(i.val+1))))
      (arithmeticPrimePatterns B M u) (fun p => (u : ZMod p.val))) :
    actualCandidateKernel B L T H M τ C χ u =
…

Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.blockCandidates, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.CandidateForcedWitness, OAI.JointDickman.ArithmeticCoefficientHit, OAI.JointDickman.candidateArithmeticQuotient, OAI.JointDickman.MaskedCoefficientEvent, OAI.JointDickman.arithmeticPrimePatterns, OAI.JointDickman.actualCandidateKernel