phaseBudgetEngine

formal source

  51/-- A minimal visibility engine (KTheta floor hypothesis + stable budget) supplies the
  52`PhaseBudgetEngine` directly.  The bound field receives the gate witness
  53itself, so the membership check is satisfied by reflexivity. -/
  54noncomputable def phaseBudgetEngine (engine : MinimalEngine) :
  55    PhaseBudgetToErdosStraus.PhaseBudgetEngine where
  56  bound := fun n =>
  57    if h : ResidualTrap n then
  58      Classical.choose (subset_product_hit_of_minimal engine
  59        (nonIdentityReciprocal_of_residualTrap h))
  60    else 0
  61  supplies_hit := by
  62    intro n hntrap
  63    have hn : NonIdentityReciprocal n :=
  64      nonIdentityReciprocal_of_residualTrap hntrap
  65    have hex := subset_product_hit_of_minimal engine hn
  66    refine ⟨Classical.choose hex, ?_, ?_, ?_⟩
  67    · simp [hntrap]
  68    · exact (Classical.choose_spec hex).1
  69    · exact (Classical.choose_spec hex).2
  70
  71/-- Final closure: a minimal visibility engine solves the residual class. -/
  72theorem erdos_straus_residual_from_minimal_engine
  73    (engine : MinimalEngine)
  74    {n : ℕ} (hn : ResidualTrap n) :
  75    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  76  PhaseBudgetToErdosStraus.erdos_straus_residual_from_phaseBudget
  77    (phaseBudgetEngine engine) hn
  78
  79end MinimalVisibilityEngine
  80end NumberTheory
  81end IndisputableMonolith