limitativeResult_count
plain-language theorem explainer
The theorem asserts that the inductive type of limitative results on formal systems contains exactly five elements. Researchers examining structural constraints on provability within Recognition Science-derived mathematics would cite this count. The proof is a one-line decision procedure that evaluates the Fintype cardinality directly from the five constructors.
Claim. The finite type enumerating the five limitative results (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) has cardinality 5.
background
The module supplies a structural reference for Gödel incompleteness theorems and related limitative results inside Recognition Science. It introduces the inductive type LimitativeResult whose five constructors are godelFirst, godelSecond, tarskiUndefinability, churchUndecidability, and turingHalting; the type derives Fintype so that its cardinality is computable. The module documentation states that these five results correspond to configDim D = 5 and that each imposes a distinct limit on formal systems, with Lean status zero sorry and zero axiom.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression for LimitativeResult, which reduces immediately because the inductive type has five constructors and derives Fintype.
why it matters
The result supplies the integer 5 to the downstream definition godelTheoremsCert via the field five_results. It completes the enumeration step in the module's structural reference for the five limitative results (= configDim D = 5). Within the Recognition Science framework this count aligns with the overall architecture of limits derived from the forcing chain, though the declaration itself does not invoke T0-T8 or the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.