IndisputableMonolith.Mathematics.GodelTheoremsStructuralFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Five Classical Limitative Results — Structural Reference
   6
   7This module records the five canonical limitative-result theorems of
   820th-century mathematical logic as a five-constructor inductive type,
   9together with a cardinality theorem `Fintype.card LimitativeResult = 5`.
  10
  11The five constructors:
  12
  13- `godelFirst`: Gödel's first incompleteness theorem (1931).
  14- `godelSecond`: Gödel's second incompleteness theorem (1931).
  15- `tarskiUndefinability`: Tarski's undefinability of truth (1933).
  16- `churchUndecidability`: Church's undecidability of the Entscheidungsproblem (1936).
  17- `turingHalting`: Turing's halting problem (1936).
  18
  19## What this module is
  20
  21A bare counting fact. It enumerates the five named limitative results
  22and proves they form a five-element finite type. It is the kind of
  23structural reference used to plug into dimension-counting bridges
  24(`configDim D = 5`) elsewhere in the framework.
  25
  26## What this module is NOT
  27
  28It is **not** a claim that Recognition Science evades any of these five
  29results. None of the five constructors carries a proof that the
  30corresponding theorem fails to apply to RS. The names are labels
  31attached to constructors of a five-element inductive type; they have
  32the same logical content as the labels on a `Fin 5`.
  33
  34For the honest analysis of how Gödel I and Tarski's undefinability
  35interact with Recognition Science (the categorical argument about
  36target classes, and the fact that the recovered arithmetic in
  37`RS_Arithmetic_From_Law_Of_Logic.pdf` inherits Gödel I just as PA does),
  38see `papers/Godel_And_RS_Closure_Honest_Assessment_20260520.html`.
  39
  40Lean status: 0 sorry, 0 axiom.
  41-/
  42
  43namespace IndisputableMonolith.Mathematics.GodelTheoremsStructuralFromRS
  44
  45inductive LimitativeResult where
  46  | godelFirst
  47  | godelSecond
  48  | tarskiUndefinability
  49  | churchUndecidability
  50  | turingHalting
  51  deriving DecidableEq, Repr, BEq, Fintype
  52
  53theorem limitativeResult_count :
  54    Fintype.card LimitativeResult = 5 := by decide
  55
  56structure GodelTheoremsCert where
  57  five_results : Fintype.card LimitativeResult = 5
  58
  59def godelTheoremsCert : GodelTheoremsCert where
  60  five_results := limitativeResult_count
  61
  62end IndisputableMonolith.Mathematics.GodelTheoremsStructuralFromRS
  63