canonicalMeasureCount
plain-language theorem explainer
Recognition Science admits exactly five canonical measures. A researcher building the measure-theoretic layer for J-cost integration would cite this cardinality when fixing the dimension of the measure space. The proof is a one-line decidable computation on the Fintype instance of the inductive enumeration.
Claim. The set of canonical measures has cardinality five, consisting of the Lebesgue, counting, Dirac, Hausdorff, and Borel measures.
background
The module Measure Theory from RS treats measure theory as the foundation for probability and integration inside Recognition Science, with the J-cost function positioned as a measure-theoretic object. Five canonical measures are introduced explicitly: Lebesgue, counting, Dirac, Hausdorff, and Borel, whose number equals the configuration dimension D = 5. The inductive type CanonicalMeasure enumerates these five cases and derives the Fintype instance used for cardinality.
proof idea
The proof is a one-line term that invokes the decide tactic on the Fintype.card expression. The tactic evaluates the derived Fintype instance on the inductive type whose five constructors are Lebesgue, counting, Dirac, Hausdorff, and Borel.
why it matters
This result populates the five_measures field inside the measureTheoryCert definition, which also records jcost_nonneg. It directly supports the module claim that five measures equal configDim D = 5 and supplies the enumeration needed for J-cost to be treated as a measurable object in the Recognition Science setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.