IndisputableMonolith.Materials.CorrosionMechanismsFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Corrosion Mechanisms from configDim — B9 Materials Depth
   6
   7Five canonical corrosion mechanisms (= configDim D = 5):
   8  uniform (general), galvanic, pitting, crevice,
   9  stress corrosion cracking.
  10
  11Lean status: 0 sorry, 0 axiom.
  12-/
  13
  14namespace IndisputableMonolith.Materials.CorrosionMechanismsFromConfigDim
  15
  16inductive CorrosionMechanism where
  17  | uniform
  18  | galvanic
  19  | pitting
  20  | crevice
  21  | stressCorrosionCracking
  22  deriving DecidableEq, Repr, BEq, Fintype
  23
  24theorem corrosionMechanism_count :
  25    Fintype.card CorrosionMechanism = 5 := by decide
  26
  27structure CorrosionMechanismsCert where
  28  five_mechanisms : Fintype.card CorrosionMechanism = 5
  29
  30def corrosionMechanismsCert : CorrosionMechanismsCert where
  31  five_mechanisms := corrosionMechanism_count
  32
  33end IndisputableMonolith.Materials.CorrosionMechanismsFromConfigDim
  34