No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
36theorem failureModeCount : Fintype.card InstitutionalFailureMode = 5 := by decide
proof body
Term-mode proof.
37
38/-- Three binary governance criteria (analogous to Arrow's conditions). -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
-
failureModeCount
in IndisputableMonolith.Engineering.StructuralSafetyFromJCost
decl_use
-
structuralSafetyCert
in IndisputableMonolith.Engineering.StructuralSafetyFromJCost
decl_use
-
failureModeCount
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
governanceCert
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
failureModeCount
in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost
decl_use
-
fatigueFractureCert
in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost
decl_use
-
governanceDesignCert
in IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim
decl_use
depends on (4)
Lean names referenced from this declaration's body.
-
failureModeCount
in IndisputableMonolith.Engineering.StructuralSafetyFromJCost
decl_use
-
failureModeCount
in IndisputableMonolith.Governance.InstitutionalFailureFromJCost
decl_use
-
failureModeCount
in IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost
decl_use
-
InstitutionalFailureMode
in IndisputableMonolith.Sociology.GovernanceDesignFromConfigDim
decl_use