AssessmentTypesCert
plain-language theorem explainer
The structure certifies that the enumeration of assessment types has cardinality five, consisting of diagnostic, formative, summative, criterion-referenced, and portfolio cases. Education modelers in the Recognition Science framework cite it to fix the assessment cycle at configDim equal to five. The declaration is a direct structure definition that inherits the finite cardinality from the derived Fintype instance on the enumeration.
Claim. The certificate structure is defined by the single field asserting that the finite cardinality of the assessment type collection equals five, where the collection consists of the five cases diagnostic, formative, summative, criterion-referenced, and portfolio.
background
In the Education module, assessment types form an inductive enumeration whose five constructors match the configuration dimension of five. The cases are diagnostic for baseline evaluation, formative for feedback during instruction, summative for certification, criterion-referenced for standard alignment, and portfolio for longitudinal records; these span the full practical assessment cycle. The module states that this enumeration carries a derived Fintype instance whose cardinality computation yields exactly five.
proof idea
The declaration is a structure definition with an empty proof body. It directly encodes the cardinality assertion by referencing the Fintype.card computation on the assessment type enumeration, which evaluates to five from the five constructors.
why it matters
The structure supplies the type for the downstream assessmentTypesCert definition, which constructs an explicit instance by assigning the computed count to the field. It anchors the education module at five dimensions inside the Recognition Science framework, consistent with the configDim convention for assessment cycles. No direct link to the T0-T8 forcing chain or RCL appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.