pith. machine review for the scientific record. sign in
def definition def or abbrev

phaseBudgetEngine

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  54noncomputable def phaseBudgetEngine (engine : MinimalEngine) :
  55    PhaseBudgetToErdosStraus.PhaseBudgetEngine where
  56  bound := fun n =>

proof body

Definition body.

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.