PedagogyModel
plain-language theorem explainer
The PedagogyModel inductive type enumerates five canonical pedagogy models aligned with configDim equal to 5. Each model maps to a distinct recognition channel in the education framework. Researchers extending Recognition Science to pedagogical structures cite this enumeration to certify model counts and certification records. The declaration is a direct inductive definition deriving Fintype for immediate cardinality verification.
Claim. Let $M$ be the finite set of pedagogy models consisting of direct instruction, mastery learning, inquiry-based learning, project-based learning, and apprenticeship, equipped with decidable equality and finite type structure.
background
In the Recognition Science framework, configDim is the dimensionality parameter for educational configurations, fixed here at 5 to match the five listed models. The module associates each model with a distinct recognition channel: exposition, practice, exploration, synthesis, and enculturation. This supplies the base enumeration for downstream cardinality and certification results in the education domain.
proof idea
The declaration is an inductive definition that introduces five constructors and derives DecidableEq, Repr, BEq, and Fintype instances in a single step.
why it matters
This definition supplies the enumeration required by the pedagogyModel_count theorem asserting cardinality exactly 5 and by the PedagogyModelsCert structure. It realizes the E5 education depth by tying configDim to five recognition channels. The step closes the enumeration prerequisite for education certifications without introducing open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.