BoundedFiniteQuotientPhaseVisibility

formal source

  36
  37/-- A bounded visibility package: a gate below `bound n` with a concrete
  38subset-product phase hit. -/
  39def BoundedFiniteQuotientPhaseVisibility (n : ℕ) (bound : ℕ → ℕ) : Prop :=
  40  ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c)
  41
  42/-- The exact bounded visibility theorem.  The proof uses the floor/budget
  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)