structure definition def or abbrev

`PhaseBudgetEngineLogic`

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

formal statement (Lean)

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

used by (2)

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

erdos_straus_residual_from_phaseBudget_logic in IndisputableMonolith.NumberTheory.LogicPhaseBudgetBridge decl_use
toClassicalEngine in IndisputableMonolith.NumberTheory.LogicPhaseBudgetBridge decl_use

depends on (5)

Lean names referenced from this declaration's body.

LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
PhaseBudgetEngine in IndisputableMonolith.NumberTheory.PhaseBudgetToErdosStraus decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use