IndisputableMonolith.Materials.AdditiveManufacturingDefectsFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Additive Manufacturing Defects from configDim — Materials Depth
   6
   7Five canonical additive-manufacturing defect classes (= configDim D = 5):
   8  porosity, lack-of-fusion, keyhole voids, residual stress, surface roughness.
   9
  10These cover volumetric, interlayer, vapor-cavity, mechanical, and boundary
  11defects in metal and polymer printing.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Materials.AdditiveManufacturingDefectsFromConfigDim
  17
  18inductive AdditiveDefect where
  19  | porosity
  20  | lackOfFusion
  21  | keyholeVoid
  22  | residualStress
  23  | surfaceRoughness
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem additiveDefect_count : Fintype.card AdditiveDefect = 5 := by decide
  27
  28structure AdditiveManufacturingDefectsCert where
  29  five_defects : Fintype.card AdditiveDefect = 5
  30
  31def additiveManufacturingDefectsCert : AdditiveManufacturingDefectsCert where
  32  five_defects := additiveDefect_count
  33
  34end IndisputableMonolith.Materials.AdditiveManufacturingDefectsFromConfigDim
  35