RsCategoricalDifferenceFromGodel
plain-language theorem explainer
Documentation record listing three categorical mismatches between Recognition Science and the target class of Gödel's first incompleteness theorem: RS is selection dynamics rather than a proof system, its truth notion is stabilization rather than Tarskian satisfaction, and truth is internal with no external model. Anyone arguing that Gödel I does not apply inside the RS forcing chain would cite this bundle. It is a bare structure of Props with no proof content; the canonical inhabitant simply fills each field with True.
Claim. A documentation record consisting of three propositions: (i) Recognition Science is selection dynamics, not a formal proof system; (ii) RS truth is stabilization of configurations, not Tarskian model satisfaction; (iii) RS truth is internal and requires no external model. The structure carries no theorem content; its canonical inhabitant sets each field to $\mathrm{True}$.
background
The ambient module proves a classical-logic fact: no real configuration $c$ can satisfy $(\mathrm{defect},c = 0) \leftrightarrow \neg(\mathrm{defect},c = 0)$, by a two-line case split on excluded middle. The same holds for any predicate $P$: classical logic has no fixed point of negation. That content is propositional logic, not RS-specific physics.
The module doc is explicit that this does not address Gödel I. Gödel sentences satisfy $G \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a relation between a sentence and a syntactic provability predicate, not $P \leftrightarrow \neg P$. The historical filename GodelDissolution was therefore misleading; the honest categorical argument that Gödel I has no target inside the RS forcing chain (T-1 through T8 and the derived constants) lives at the meta-level, outside Lean.
This structure packages the three meta-level mismatches as named Prop fields so downstream shims and the honest-assessment paper can point at a single Lean object without pretending the claims are proved theorems.
proof idea
There is no proof. The declaration is a structure of three bare Prop fields. A sibling definition supplies the canonical inhabitant by setting not_proof_system, not_tarskian, and no_external_model each to True. No lemmas are applied; no tactics run.
why it matters
The structure exists so the framework can name, without overclaiming, why Gödel I is not aimed at the RS forcing chain. Downstream, the canonical inhabitant rs_categorical_difference_from_godel fills every field with True, and the deprecated shims GodelRequirements and RSDoesNotSatisfyGodel in GodelDissolution re-export related documentation records under old names.
In the primer landmarks, the forcing chain T0–T8 (J-uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$) is a selection dynamics on cost and recognition, not a recursively axiomatized arithmetic theory with a Tarskian satisfaction relation. Citing this record keeps that distinction visible while the module's actual theorems stay limited to the biconditional self-negation fact and its corollaries about zero-defect configurations.
The open question it touches is meta-level only: whether a fully formalized categorical non-applicability argument could ever be internalized in Lean. The module doc points to the honest assessment note rather than claiming such a theorem here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.