logicSystem_count
plain-language theorem explainer
The theorem establishes that the inductive enumeration of logic systems tied to configuration dimension 5 has cardinality exactly 5. Researchers mapping configDim to canonical logics in Recognition Science would cite this cardinality. The proof is a one-line decide tactic on the derived Fintype instance of the five-constructor inductive type.
Claim. The set of logic systems has cardinality five: $|$ {propositional, first-order, second-order, modal, intuitionistic} $| = 5$.
background
The module introduces five canonical logic systems corresponding to configDim D = 5. LogicSystem is the inductive type with constructors propositional, first-order, second-order, modal, intuitionistic, deriving DecidableEq, Repr, BEq, and Fintype. This sits in the local setting of mathematical logic systems from configDim, with zero sorry or axiom in the module.
proof idea
The proof is a one-line wrapper that applies the decide tactic, which computes Fintype.card directly from the derived Fintype instance on the inductive type.
why it matters
This populates the five_systems field of logicSystemsCert. It supports the framework identification of exactly five logic systems at configDim D = 5, consistent with the eight-tick octave and D = 3 spatial dimensions in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.