BoundedVisibilityEngine

formal source

  43interfaces as inputs; the witness itself is supplied by the phase-budget
  44engine field because budget arithmetic bounds failed gates but does not
  45construct the subset-product divisor. -/
  46structure BoundedVisibilityEngine where
  47  bound : ℕ → ℕ
  48  costOf : ℕ → ℕ → ℝ
  49  stable :
  50    ∀ n : ℕ, NonIdentityReciprocal n → StableIntegerLedgerBudget n (costOf n)
  51  floor :
  52    ∀ n : ℕ, NonIdentityReciprocal n → KThetaFailureFloorHypothesis n (costOf n)
  53  visibility :
  54    ∀ n : ℕ, NonIdentityReciprocal n → BoundedFiniteQuotientPhaseVisibility n bound
  55
  56/-- A bounded visibility engine proves bounded phase visibility for every
  57nonidentity reciprocal ledger. -/
  58theorem bounded_phase_visibility
  59    (engine : BoundedVisibilityEngine)
  60    {n : ℕ} (hn : NonIdentityReciprocal n) :
  61    BoundedFiniteQuotientPhaseVisibility n engine.bound :=
  62  engine.visibility n hn
  63
  64/-- Under the explicit KTheta floor hypothesis and stable budget interfaces, failed gates in a
  65finite set have total cost bounded by the stable budget. -/
  66theorem failed_gate_count_bounded_at_KTheta
  67    {n : ℕ} {costOf : ℕ → ℝ} {S : Finset ℕ}
  68    (stable : StableIntegerLedgerBudget n costOf)
  69    (floor : KThetaFailureFloorHypothesis n costOf)
  70    (hfails : ∀ c ∈ S, GateFails n c) :
  71    KTheta * (S.card : ℝ) ≤ stable.budget := by
  72  apply failed_gate_count_bounded_by_budget stable
  73  exact ⟨KTheta_pos, hfails, fun c hc => floor.floor c (hfails c hc)⟩
  74
  75end BoundedPhaseVisibility
  76end NumberTheory