structure definition def or abbrev

`CorrectionProtocol`

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

formal statement (Lean)

  70structure CorrectionProtocol (X : Ω → ℝ) where
  71  /-- The correction map -/
  72  correct : Ω → Ω
  73  /-- Correction reduces or preserves cost -/
  74  cost_decreasing : ∀ ω, Jcost (X (correct ω)) ≤ Jcost (X ω)
  75  /-- Ground states are fixed points -/
  76  ground_fixed : ∀ ω, Jcost (X ω) = 0 → correct ω = ω
  77
  78/-- The 8-tick correction cycle.
  79    After 8 ticks, the system has had a full opportunity to correct errors. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

conservation_is_protected in IndisputableMonolith.Thermodynamics.ErrorCorrection decl_use
is_complete_correction in IndisputableMonolith.Thermodynamics.ErrorCorrection decl_use
is_fault_tolerant in IndisputableMonolith.Thermodynamics.ErrorCorrection decl_use
is_protected_observable in IndisputableMonolith.Thermodynamics.ErrorCorrection decl_use

depends on (8)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
or in IndisputableMonolith.Constants.EulerMascheroni decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use