inductive definition def or abbrev

`FailureMode`

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

formal statement (Lean)

  93inductive FailureMode where
  94  | singleAxisDecoderSuffices
  95  | noSmallPhiPowerRatio
  96  | additiveTherapyResponse
  97  | depthExceedsFiveBits
  98  | nonFortyPlateauSpectrum
  99  | nonReverseDementiaOrder
 100  | nonUnitSharedCoefficient
 101  | nonQSpaceSpanCollapse
 102  | moduleExceedsCeiling70
 103  deriving DecidableEq, Repr, Fintype
 104

used by (15)

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

FailureMode in IndisputableMonolith.Engineering.StructuralSafetyFromJCost decl_use
failureModeCount in IndisputableMonolith.Engineering.StructuralSafetyFromJCost decl_use
StructuralSafetyCert in IndisputableMonolith.Engineering.StructuralSafetyFromJCost decl_use
ProtocolFalsifiable in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
ProtocolSpec in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
failureMode in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
failureMode_count in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
FalsifierRegistryCert in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
FailureMode in IndisputableMonolith.Governance.InstitutionalFailureFromJCost decl_use
failureModeCount in IndisputableMonolith.Governance.InstitutionalFailureFromJCost decl_use
GovernanceCert in IndisputableMonolith.Governance.InstitutionalFailureFromJCost decl_use
institutionFailureMode in IndisputableMonolith.Governance.InstitutionalFailureFromJCost decl_use
FailureMode in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost decl_use
failureModeCount in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost decl_use
FatigueFractureCert in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost decl_use

depends on (3)

Lean names referenced from this declaration's body.

FailureMode in IndisputableMonolith.Engineering.StructuralSafetyFromJCost decl_use
FailureMode in IndisputableMonolith.Governance.InstitutionalFailureFromJCost decl_use
FailureMode in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost decl_use