`PhaseBudgetEngineLogic`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.LogicPhaseBudgetBridge
domain: NumberTheory
line: 27 · 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 27.

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

used by

formal source

  24/-- Logic-native phase-budget engine. The bound and input carrier are
  25`LogicNat`; the actual finite gate witness is transported to the existing
  26classical engine surface. -/
  27structure PhaseBudgetEngineLogic where
  28  bound : LogicNat → LogicNat
  29  classical_engine : PhaseBudgetToErdosStraus.PhaseBudgetEngine
  30  bound_compat : ∀ n : LogicNat, toNat (bound n) = classical_engine.bound (toNat n)
  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.