assessmentType_count
plain-language theorem explainer
assessmentType_count establishes that the finite type AssessmentType has cardinality exactly five, matching the configDim parameter D=5 for the education module. Education modelers formalizing assessment cycles would cite this result when confirming that the five modes cover baseline through longitudinal tracking. The proof is a one-line decision tactic that computes the cardinality from the derived Fintype instance on the inductive definition.
Claim. The finite cardinality of the assessment type enumeration is five: $ |AssessmentType| = 5 $, where AssessmentType is the inductive type with constructors diagnostic, formative, summative, criterion-referenced, and portfolio.
background
The module sets configDim to five to align with five canonical assessment types that span the practical cycle: baseline measurement, ongoing feedback, final certification, standard comparison, and longitudinal portfolio tracking. AssessmentType is defined as an inductive type with exactly those five constructors and automatically derives Fintype, DecidableEq, and related instances. This local setting applies the Recognition Science dimensional assignment pattern to the education domain.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds directly because the inductive definition yields a Fintype instance whose cardinality is computable by enumeration of the five constructors.
why it matters
This theorem supplies the concrete cardinality value assigned to five_types in the downstream assessmentTypesCert definition, which constructs the AssessmentTypesCert certificate. It fills the E5 education depth slot, consistent with the framework's use of integer dimensions fixed by the forcing chain and eight-tick octave. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.