assessmentTypesCert
plain-language theorem explainer
The definition supplies a concrete certificate that exactly five assessment types exist for the education sector of the Recognition Science model. Modelers working on assessment cycles in the E5 depth would cite it to lock configDim to 5. The construction is a one-line definition that directly assigns the structure field from the decidable cardinality theorem.
Claim. Let AssessmentTypesCert be the structure whose sole field requires that the finite cardinality of the assessment-type enumeration equals 5. The definition instantiates this structure by setting the field to the value of the cardinality theorem.
background
The module defines five canonical assessment types (diagnostic, formative, summative, criterion-referenced, portfolio) that span the practical cycle of baseline measurement, feedback, certification, standard matching, and longitudinal artifacts. This collection is tied to configDim equal to 5. The upstream theorem assessmentType_count establishes the cardinality result by decision procedure on the enumerated type.
proof idea
The definition is a one-line wrapper that constructs the AssessmentTypesCert record by assigning its five_types field directly to the result of the assessmentType_count theorem.
why it matters
This definition completes the education assessment section by certifying the dimension-5 count. It parallels other dimension certifications in the framework (such as spatial D=3 from T8) and supplies the required witness for the AssessmentTypesCert structure. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.