LogicSystemsCert
plain-language theorem explainer
LogicSystemsCert is a structure that certifies the finite type of logic systems has cardinality exactly five. Researchers deriving logic from Recognition Science configuration dimension would cite it to connect configDim = 5 with the five enumerated systems. The declaration is a direct structure definition containing one field that encodes the cardinality condition.
Claim. A structure $LogicSystemsCert$ with a field asserting that the cardinality of the finite type of logic systems equals 5, where the logic systems are the inductive enumeration consisting of propositional, first-order, second-order, modal, and intuitionistic logic.
background
Recognition Science sets configDim = 5 to match five canonical logic systems. The local inductive type LogicSystem enumerates them as propositional, firstOrder, secondOrder, modal, and intuitionistic, and derives Fintype, DecidableEq, and related instances. The module documentation states that these five systems arise directly from the dimensional parameter, while the upstream structure from UltimateIsomorphism supplies a simplified model with propositions and a provability relation.
proof idea
The declaration is a structure definition whose single field requires Fintype.card LogicSystem = 5. No lemmas or tactics are invoked; it functions as a type wrapper that downstream definitions instantiate directly.
why it matters
LogicSystemsCert supplies the type for the downstream logicSystemsCert definition, which populates the field via logicSystem_count. It formalizes the module's claim that configDim = 5 yields precisely the five listed logic systems, supporting the Recognition Science step that extracts logic from the forcing chain after T8 dimensional configuration. The spatial dimension remains D = 3 while this configDim governs the logic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.