MinimalEngine

formal source

  26
  27/-- A minimal visibility engine carries only KTheta floor hypothesis and stable budget.  No
  28visibility field. -/
  29structure MinimalEngine where
  30  costOf : ℕ → ℕ → ℝ
  31  stable :
  32    ∀ n : ℕ, NonIdentityReciprocal n → StableIntegerLedgerBudget n (costOf n)
  33  floor :
  34    ∀ n : ℕ, NonIdentityReciprocal n → KThetaFailureFloorHypothesis n (costOf n)
  35
  36/-- A minimal engine yields a successful admissible gate for every
  37nonidentity reciprocal ledger. -/
  38theorem hits_admissible_gate (engine : MinimalEngine)
  39    {n : ℕ} (hn : NonIdentityReciprocal n) :
  40    ∃ c : ℕ, AdmissibleHardGate c ∧ HitsBalancedPhase n c :=
  41  hits_balanced_phase_of_floor_and_budget hn (engine.stable n hn) (engine.floor n hn)
  42
  43/-- A successful admissible gate gives a `SubsetProductPhaseHit` witness. -/
  44theorem subset_product_hit_of_minimal (engine : MinimalEngine)
  45    {n : ℕ} (hn : NonIdentityReciprocal n) :
  46    ∃ c : ℕ, AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c) := by
  47  classical
  48  rcases hits_admissible_gate engine hn with ⟨c, hc, hhit⟩
  49  exact ⟨c, hc, subsetProductPhaseHit_of_hitsBalancedPhase hhit⟩
  50
  51/-- A minimal visibility engine (KTheta floor hypothesis + stable budget) supplies the
  52`PhaseBudgetEngine` directly.  The bound field receives the gate witness
  53itself, so the membership check is satisfied by reflexivity. -/
  54noncomputable def phaseBudgetEngine (engine : MinimalEngine) :
  55    PhaseBudgetToErdosStraus.PhaseBudgetEngine where
  56  bound := fun n =>
  57    if h : ResidualTrap n then
  58      Classical.choose (subset_product_hit_of_minimal engine
  59        (nonIdentityReciprocal_of_residualTrap h))