primePhaseBoxDistribution_of_effectivePrimePhaseInput

formal source

  32
  33/-- Effective prime phase supply gives the exact distribution statement
  34required by the residual Erdős-Straus chain. -/
  35def primePhaseBoxDistribution_of_effectivePrimePhaseInput
  36    (input : EffectivePrimePhaseInput) :
  37    PrimePhaseBoxDistribution where
  38  bound := input.bound
  39  hits := by
  40    intro n hn
  41    rcases input.supplies_generators n hn with ⟨c, hcbound, hc, ⟨hit⟩⟩
  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