pedagogyModelsCert
plain-language theorem explainer
The definition pedagogyModelsCert builds a certificate asserting exactly five pedagogy models exist for configDim equal to 5. Education theorists working with Recognition Science channels would cite it to anchor canonical teaching approaches to distinct recognition modes. The construction is a direct one-line assignment that populates the single field of the PedagogyModelsCert structure from a decidable cardinality theorem.
Claim. Let $PedagogyModelsCert$ be the structure whose sole field requires that the cardinality of the type of pedagogy models equals 5. The definition $pedagogyModelsCert$ is the instance of this structure in which the field is set to the value of the theorem establishing that cardinality.
background
The module Pedagogy Models from configDim treats education depth as configDim equal to 5. It enumerates five canonical pedagogy models, each tied to one recognition channel: direct instruction for exposition, mastery learning for practice, inquiry-based learning for exploration, project-based learning for synthesis, and apprenticeship for enculturation. The upstream theorem pedagogyModel_count establishes that the cardinality of the PedagogyModel type is exactly 5 by a decidable computation. The sibling structure PedagogyModelsCert packages this cardinality assertion as a single-field record.
proof idea
The definition is a one-line wrapper that applies the theorem pedagogyModel_count to supply the five_models field of the PedagogyModelsCert structure.
why it matters
This definition supplies the concrete certificate for the E5 education depth inside the Recognition Science framework. It realizes the five-model count required by configDim equal to 5 and thereby links the framework's recognition channels to standard pedagogy. No downstream uses are recorded yet, leaving open how the certificate will be invoked in larger education or learning-theory developments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.