`effectivePrimePhaseInput_of_phaseBudgetEngine`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.PhaseBudgetToErdosStraus
domain: NumberTheory
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.PhaseBudgetToErdosStraus on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  34      ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c)
  35
  36/-- A phase-budget engine is exactly an effective prime phase input. -/
  37def effectivePrimePhaseInput_of_phaseBudgetEngine
  38    (engine : PhaseBudgetEngine) :
  39    EffectivePrimePhaseInput where
  40  bound := engine.bound
  41  supplies_generators := engine.supplies_hit
  42
  43/-- A phase-budget engine supplies bounded balanced search. -/
  44def boundedBalancedSearch_of_phaseBudget
  45    (engine : PhaseBudgetEngine) :
  46    BoundedBalancedSearchEngine :=
  47  boundedBalancedSearch_of_effectivePrimePhaseInput
  48    (effectivePrimePhaseInput_of_phaseBudgetEngine engine)
  49
  50/-- A phase-budget engine solves the residual trapped class. -/
  51theorem erdos_straus_residual_from_phaseBudget
  52    (engine : PhaseBudgetEngine)
  53    {n : ℕ} (hn : ResidualTrap n) :
  54    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  55  erdos_straus_residual_from_effectivePrimePhaseInput
  56    (effectivePrimePhaseInput_of_phaseBudgetEngine engine) hn
  57
  58end PhaseBudgetToErdosStraus
  59end NumberTheory
  60end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.