boundedBalancedSearch_of_effectivePrimePhaseInput

formal source

  42    exact ⟨c, hcbound, hc, generated_phase_hit_gives_HitsBalancedPhase hit⟩
  43
  44/-- Effective prime phase supply gives bounded balanced search. -/
  45def boundedBalancedSearch_of_effectivePrimePhaseInput
  46    (input : EffectivePrimePhaseInput) :
  47    BoundedBalancedSearchEngine :=
  48  boundedBalancedSearch_of_primePhaseBoxDistribution
  49    (primePhaseBoxDistribution_of_effectivePrimePhaseInput input)
  50
  51/-- Effective prime phase supply solves the residual trapped class. -/
  52theorem erdos_straus_residual_from_effectivePrimePhaseInput
  53    (input : EffectivePrimePhaseInput)
  54    {n : ℕ} (hn : ResidualTrap n) :
  55    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  56  erdos_straus_residual_from_prime_phase_box_distribution
  57    (primePhaseBoxDistribution_of_effectivePrimePhaseInput input) hn
  58
  59/-- The intended RS source theorem.  This is the final remaining input:
  60derive `EffectivePrimePhaseInput` from the RCL prime-ledger machinery. -/
  61structure RSPrimePhaseEquidistribution where
  62  effective_input : EffectivePrimePhaseInput
  63  /-- Marker: this theorem is meant to be sourced from RCL/J-cost prime-ledger
  64  phase distribution, not from finite search. -/
  65  from_rcl_prime_ledger : True
  66
  67def effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution
  68    (rs : RSPrimePhaseEquidistribution) :
  69    EffectivePrimePhaseInput :=
  70  rs.effective_input
  71
  72theorem erdos_straus_residual_from_rsPrimePhaseEquidistribution
  73    (rs : RSPrimePhaseEquidistribution)
  74    {n : ℕ} (hn : ResidualTrap n) :
  75    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=