IndisputableMonolith.NumberTheory.PhaseBudgetToErdosStraus

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.EffectivePrimePhaseInput
   3import IndisputableMonolith.NumberTheory.T1PhaseBudgetBound
   4
   5/-!
   6# Phase Budget to Erdős-Straus
   7
   8This module composes the phase-budget interface with the already-proved
   9Erdős-Straus RCL closure chain.
  10
  11The result is conditional on a `PhaseBudgetEngine`: an explicit package saying
  12that the T1/RCL budget, uniform failure floor, and finite gate enumeration
  13produce a bounded subset-product phase hit for every residual trap.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace PhaseBudgetToErdosStraus
  19
  20open ErdosStrausRotationHierarchy
  21open SubsetProductPhase
  22open PrimePhaseInput
  23
  24/-- A phase-budget engine supplies the actual bounded subset-product hit.
  25
  26The previous modules prove why such an engine is enough: finite phase
  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
  61