structure definition def or abbrev

`ProtocolSpec`

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

formal statement (Lean)

  24structure ProtocolSpec where
  25  dataset : DatasetClass
  26  observable : PredictedObservable
  27  failure : FailureMode
  28  deriving DecidableEq, Repr
  29
  30/-- The empirical protocol associated to a combination. -/

used by (8)

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

PipelineSpec in IndisputableMonolith.Foundation.OptionAEmpiricalPipeline decl_use
ProgramSpec in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
c3_uniqueProtocol in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
EmpiricalProtocolCert in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
ProtocolMatches in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
protocolSpec in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
protocolSpec_injective in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
uniqueProtocolSpec in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use

depends on (6)

Lean names referenced from this declaration's body.

FailureMode in IndisputableMonolith.Engineering.StructuralSafetyFromJCost decl_use
DatasetClass in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
FailureMode in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
PredictedObservable in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
FailureMode in IndisputableMonolith.Governance.InstitutionalFailureFromJCost decl_use
FailureMode in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost decl_use