limitativeResult_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove any of the five individual limitative results.
- Does not derive the results from the Recognition Science functional equation.
- Does not determine whether Recognition Science itself is subject to these limits.
- Does not address consistency or completeness of the ambient formal system.
formal statement (Lean)
28theorem limitativeResult_count :
29 Fintype.card LimitativeResult = 5 := by decide
proof body
30