IndisputableMonolith.NumberTheory.ErdosStrausResidualClosed

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.PhaseBudgetEngineFromRS
   3
   4/-!
   5# Erdős-Straus Residual Closure
   6
   7Final residual theorem, conditional on the recovered-ledger bounded visibility
   8engine.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace NumberTheory
  13namespace ErdosStrausResidualClosed
  14
  15open ErdosStrausRotationHierarchy
  16open BoundedPhaseVisibility
  17open PhaseBudgetEngineFromRS
  18
  19/-- Conditional residual closure: once bounded phase visibility is supplied
  20for recovered integer ledgers, every residual trapped `n` has an
  21Erdős-Straus representation. -/
  22theorem erdos_straus_residual_closed
  23    (engine : BoundedVisibilityEngine)
  24    {n : ℕ} (hn : ResidualTrap n) :
  25    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  26  PhaseBudgetToErdosStraus.erdos_straus_residual_from_phaseBudget
  27    (phaseBudgetEngine_of_boundedVisibilityEngine engine) hn
  28
  29end ErdosStrausResidualClosed
  30end NumberTheory
  31end IndisputableMonolith
  32