additiveManufacturingDefectsCert
plain-language theorem explainer
This definition constructs an instance of the certificate structure asserting that the additive manufacturing defect type has cardinality exactly 5, matching configDim D=5. Materials modelers working on 3D printing defect enumeration would cite it to anchor the defect count to the Recognition Science dimension parameter. It is realized as a one-line structure constructor that inserts the decided cardinality theorem into the required field.
Claim. Let $C$ be the structure whose field requires that the finite cardinality of the additive defect type equals 5. The definition supplies the instance of $C$ whose field is populated by the theorem establishing this equality.
background
The module treats five canonical additive-manufacturing defect classes as corresponding to configDim D=5: porosity, lack-of-fusion, keyhole voids, residual stress, and surface roughness. These classes respectively cover volumetric, interlayer, vapor-cavity, mechanical, and boundary defects in metal and polymer printing. The structure AdditiveManufacturingDefectsCert is the record type whose sole field is the proposition that the cardinality of AdditiveDefect equals 5. The upstream theorem additiveDefect_count proves this cardinality by a decision procedure.
proof idea
One-line wrapper that applies the structure constructor to the theorem additiveDefect_count.
why it matters
This supplies the explicit certificate that enumerates the defect classes to match the configDim parameter inside the materials domain. It closes the local definition of the defect count with zero axioms and zero sorrys. No downstream theorems are recorded in the used-by graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.