PrimePhaseBoxDistribution

formal source

  24
  25For every residual trapped `n`, a bounded admissible gate `c` has a divisor
  26box point hitting the required balanced phase. -/
  27structure PrimePhaseBoxDistribution where
  28  bound : ℕ → ℕ
  29  hits :
  30    ∀ n : ℕ, ResidualTrap n →
  31      ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ HitsBalancedPhase n c
  32
  33/-- The exact finite-combinatorial conversion:
  34prime phase box distribution gives the bounded balanced search engine. -/
  35def boundedBalancedSearch_of_primePhaseBoxDistribution
  36    (dist : PrimePhaseBoxDistribution) :
  37    BoundedBalancedSearchEngine where
  38  bound := dist.bound
  39  bound_ok := by
  40    intro n hn
  41    rcases dist.hits n hn with ⟨c, hcbound, hc, hhit⟩
  42    exact ⟨c, hcbound, hc, box_phase_hit_gives_balanced_pair hhit⟩
  43
  44/-- If the prime phase box distribution theorem is supplied, the residual
  45Erdős-Straus class follows. -/
  46theorem erdos_straus_residual_from_prime_phase_box_distribution
  47    (dist : PrimePhaseBoxDistribution)
  48    {n : ℕ} (hn : ResidualTrap n) :
  49    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  50  bounded_balanced_search_solved
  51    (boundedBalancedSearch_of_primePhaseBoxDistribution dist) hn
  52
  53/-! ## Existing RS prime-distribution surface
  54
  55The imported prime modules currently provide:
  56
  57* prime ledger cost additivity (`PrimeCostSpectrum`);