GodelTheoremsCert
plain-language theorem explainer
The structure packages a certificate asserting that exactly five limitative results are enumerated in the inductive type. Researchers embedding incompleteness theorems into Recognition Science would cite it to confirm the count matches configuration dimension D equals 5. The definition is a direct structure declaration that sets the finite cardinality field to five.
Claim. Let $L$ be the finite set whose elements are Gödel's first incompleteness theorem, Gödel's second incompleteness theorem, Tarski's undefinability of truth, Church's undecidability of the Entscheidungsproblem, and Turing's halting problem. The structure is defined by the single field asserting that the cardinality of $L$ equals 5.
background
The module supplies a structural reference for the Gödel incompleteness theorems together with three related limitative results, for a total count of five that is identified with configuration dimension D = 5. The inductive type enumerates these as five distinct cases, each establishing a separate limit on formal systems, and the Lean development contains zero axioms and zero sorry statements. The upstream inductive definition supplies the enumeration whose cardinality is asserted by the structure field.
proof idea
The declaration is a direct structure definition whose single field is the equality Fintype.card of the inductive type equals 5. No lemmas or tactics are invoked beyond the automatic derivation of Fintype for the inductive type.
why it matters
The structure supplies the type used by the downstream definition that constructs the concrete certificate instance. It completes the packaging of the five results that align with D = 5 in the module, confirming the structural count without deriving any theorem from the J-cost function or the phi-ladder. In the Recognition Science setting this step records the fixed number of limitative results that parallels the eight-tick octave and spatial dimension constraints elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.