ActualPrimeScale.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Harmonic masses and integer endpoints for the literal prime family. These derive the trace theorem's prime-pool hypotheses from the single fixed-modulus published input.

lemma OAI.TwoPointCorrelations.centeredPrimePool_mass line 14
lemma OAI.TwoPointCorrelations.centeredPrimePool_mass_bounds line 20
lemma OAI.TwoPointCorrelations.primeSupplyCount_mul_bound line 36
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_padding_pool_mass line 43
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_pool_masses line 58
Source documentation
All pool-mass hypotheses used by the literal column trace hold for the constructed bands. The numerical eligibility predicate does not enter these estimates.
```
theorem ModFiveThetaInput.eventually_actual_pool_masses (hP : ModFiveThetaInput)
    (E : Finset ℕ) (W : ℝ) (hW : 1 ≤ W) :
    ∀ᶠ L : ℝ in atTop,
      let J := primeSupplyCount W L
…
```
Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.primeSupplyCount
lemma OAI.TwoPointCorrelations.centeredPrimeTuple_upper line 104

lemma OAI.TwoPointCorrelations.centeredPrimeTuple_complement_upper line 114

Source documentation

Removing one prime from an actual tuple only reduces its value.

lemma centeredPrimeTuple_complement_upper (E : Finset ℕ) (A W L : ℝ) (J : ℕ)
    (hA : 0 < A) (hW : 1 ≤ W) (hL : primeSupplyEndpoint A W J ≤ L)
    (x : (j : Fin J) → centeredPrimeBands E A W J j) (j : Fin J) :
    (∏ i ∈ univ.erase j, (x i).val) ≤ ⌊Real.exp (2 * L)⌋₊ := by
…

Mentions: OAI.TwoPointCorrelations.primeSupplyEndpoint, OAI.TwoPointCorrelations.centeredPrimeBands

lemma OAI.TwoPointCorrelations.paddingPairEligible_padding_upper line 123
lemma OAI.TwoPointCorrelations.actualProhibitedPrimeFamily_padding_upper line 143