theorem proved term proof

`bounded_phase_visibility`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  58theorem bounded_phase_visibility
  59    (engine : BoundedVisibilityEngine)
  60    {n : ℕ} (hn : NonIdentityReciprocal n) :
  61    BoundedFiniteQuotientPhaseVisibility n engine.bound :=

proof body

Term-mode proof.

  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. -/

depends on (9)

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
BoundedFiniteQuotientPhaseVisibility in IndisputableMonolith.NumberTheory.BoundedPhaseVisibility decl_use
BoundedVisibilityEngine in IndisputableMonolith.NumberTheory.BoundedPhaseVisibility decl_use
NonIdentityReciprocal in IndisputableMonolith.NumberTheory.BoundedPhaseVisibility decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
KTheta in IndisputableMonolith.NumberTheory.UniformFailureFloor decl_use