IndisputableMonolith.NumberTheory.LogicPhaseBudgetBridge

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.PhaseBudgetToErdosStraus
   3import IndisputableMonolith.NumberTheory.LogicErdosStrausBoxPhase
   4
   5/-!
   6  LogicPhaseBudgetBridge.lean
   7
   8  Logic-native wrapper for the Erdős-Straus phase-budget engine.
   9
  10  The existing phase-budget engine remains the computational bridge. This
  11  module packages it behind recovered-natural inputs and proves that the
  12  final residual theorem can be read as a recovered-rational theorem.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace NumberTheory
  17namespace LogicPhaseBudgetBridge
  18
  19open Foundation.ArithmeticFromLogic
  20open Foundation.ArithmeticFromLogic.LogicNat
  21open Foundation.RationalsFromLogic.LogicRat
  22open LogicErdosStrausRCL
  23
  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
  52