mediaEraCount
plain-language theorem explainer
mediaEraCount establishes that the finite type of media eras contains exactly five elements, matching McLuhan's canonical stages. Media theorists applying Recognition Science to sociology reference this cardinality when setting the configuration dimension to five. The proof reduces to a single decide tactic invocation on the enumerated inductive type.
Claim. The finite type of media eras has cardinality 5, where the type enumerates the stages oral, literary, print, electronic, and digital.
background
MediaEra is the inductive type with five constructors oral, literary, print, electronic, digital, equipped with DecidableEq, Repr, BEq, and Fintype instances. The module frames media as recognition bandwidth at successive epochs in Recognition Science, equating the five stages to configuration dimension D equals 5 and placing the digital era at rung phi^12. The sole upstream dependency is the inductive definition of MediaEra itself.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality of the finite inductive type MediaEra.
why it matters
This result supplies the five_eras field inside the mediaEcologyCert definition, anchoring the sociological extension of Recognition Science to McLuhan's stages. It directly instantiates the framework landmark that five media eras equal configDim D equals 5, with digital recognition bandwidth at phi^12 on the phi-ladder. No open questions or scaffolding are indicated in the supplied results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.