`toClassicalEngine`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.LogicPhaseBudgetBridge
domain: NumberTheory
line: 34 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.LogicPhaseBudgetBridge on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  31
  32/-- Forget the logic-native wrapper to the current classical phase-budget
  33engine. -/
  34def toClassicalEngine (engine : PhaseBudgetEngineLogic) :
  35    PhaseBudgetToErdosStraus.PhaseBudgetEngine :=
  36  engine.classical_engine
  37
  38/-- The phase-budget engine solves residual traps in the recovered rational
  39reading. -/
  40theorem erdos_straus_residual_from_phaseBudget_logic
  41    (engine : PhaseBudgetEngineLogic)
  42    {n : LogicNat}
  43    (hn : ErdosStrausRotationHierarchy.ResidualTrap (toNat n)) :
  44    HasRationalErdosStrausReprLogic (fromRat (toNat n : ℚ)) := by
  45  apply reprLogic_fromRat_of_classical
  46  exact PhaseBudgetToErdosStraus.erdos_straus_residual_from_phaseBudget
  47    engine.classical_engine hn
  48
  49end LogicPhaseBudgetBridge
  50end NumberTheory
  51end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.