PhaseBudgetEngine

formal source

  27separation, finite failure-cost accumulation, and the T1/RCL stable-budget
  28interface.  This structure is the exact remaining physical bridge from those
  29budget facts to an explicit gate witness. -/
  30structure PhaseBudgetEngine where
  31  bound : ℕ → ℕ
  32  supplies_hit :
  33    ∀ n : ℕ, ResidualTrap n →
  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