boundedBalancedSearch_of_primePhaseBoxDistribution

formal source

  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`);
  58* an RH/frustration-spectrum bridge to aggregate prime distribution
  59  (`PrimeDistributionBridge`, currently an upstream repair target under
  60  the active Lean toolchain).
  61
  62They do not yet prove the square-budget residue-box hit required above.
  63The following structure records the exact extra theorem needed from the
  64RS prime-distribution program. -/
  65