IndisputableMonolith.NumberTheory.PhaseBudgetEngineFromRS

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.BoundedPhaseVisibility
   3import IndisputableMonolith.NumberTheory.PhaseBudgetToErdosStraus
   4
   5/-!
   6# Phase Budget Engine from Recovered-Ledger Visibility
   7
   8Turns the recovered-ledger bounded visibility engine into the phase-budget
   9engine already consumed by the Erdős-Straus residual proof chain.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace NumberTheory
  14namespace PhaseBudgetEngineFromRS
  15
  16open BoundedPhaseVisibility
  17open PhaseBudgetToErdosStraus
  18open ErdosStrausRotationHierarchy
  19
  20/-- Residual traps are positive nonidentity reciprocal ledgers. -/
  21def nonIdentityReciprocal_of_residualTrap {n : ℕ} (hn : ResidualTrap n) :
  22    NonIdentityReciprocal n where
  23  pos := Nat.zero_lt_of_lt hn.1
  24  nonidentity := by
  25    intro h
  26    have hlt : 1 < 1 := by simpa [h] using hn.1
  27    omega
  28  reciprocal_budget := by
  29    exact ⟨n, Nat.zero_lt_of_lt hn.1, by
  30      exact dvd_mul_right n n⟩
  31
  32/-- A recovered-ledger bounded visibility engine supplies the phase-budget
  33engine needed by the Erdős-Straus chain. -/
  34def phaseBudgetEngine_of_boundedVisibilityEngine
  35    (engine : BoundedVisibilityEngine) :
  36    PhaseBudgetEngine where
  37  bound := engine.bound
  38  supplies_hit := by
  39    intro n hntrap
  40    exact engine.visibility n (nonIdentityReciprocal_of_residualTrap hntrap)
  41
  42/-- Bounded visibility over recovered ledgers gives bounded balanced search. -/
  43def boundedBalancedSearch_of_boundedVisibilityEngine
  44    (engine : BoundedVisibilityEngine) :
  45    BoundedBalancedSearchEngine :=
  46  boundedBalancedSearch_of_phaseBudget
  47    (phaseBudgetEngine_of_boundedVisibilityEngine engine)
  48
  49end PhaseBudgetEngineFromRS
  50end NumberTheory
  51end IndisputableMonolith
  52