ASSUMPTIONS.md

ASSUMPTIONS — modeling choices, declared

Numbered; referenced from THEOREMS.md, FIDELITY.md, and VERIFICATION.md.

A1 (Sentences as an abstract Primcodable type). A theory's sentences are represented as an abstract type S with a Primcodable instance (mathlib's standard "effectively coded" class), equipped with a computable negation map neg : S → S. We do not fix a first-order syntax. This is more general than FKSM need: every concrete first-order language with computable syntax is an instance. Nothing in their argument turns on syntax beyond the existence of negation and effective coding.

A2 ("Extends Robinson arithmetic" enters via its recursion-theoretic interface). T1 quantifies over theories that are consistent, r.e., and strongly separate a computably inseparable pair of r.e. sets (RepresentsInseparablePair in the Lean code). That any consistent r.e. extension of Q has this property is classical: the effectively inseparable pair {e : φ_e(e)=0}, {e : φ_e(e)=1} is Kleene's ("A symmetric form of Gödel's theorem", 1950; Introduction to Metamathematics §61); its strong separation in every consistent r.e. extension of Q follows from the representability of recursive functions in Q (Tarski–Mostowski–Robinson, Undecidable Theories, 1953), as developed for Rosser systems by Smullyan (Theory of Formal Systems, 1961; see also Putnam–Smullyan, Proc. AMS, 1960). We prove everything downstream of the interface in Lean with no axioms, and we exhibit a concrete instance so the hypothesis class is provably non-empty. The interface identification itself is classical prose, declared in VERIFICATION.md. Rationale: the alternative (a full arithmetization à la the Foundation library) has no bridge to mathlib's computability theory, which the simulation side of the argument requires.

A3 (Observational consequences ⊆ theorems; "consistent with" rendered as "reproduces"). The informal adequacy requirement asks only that generated streams be consistent with the theory's observational consequences. The formalized version (D3, AdequateEnum) renders it as exact reproduction: the process enumerates exactly the theorem set of T (sound: emits only theorems; complete: emits every theorem). This is sentence-level adequacy — one of two non-subsuming adequacy levels, not a stronger form of the other. World-level adequacy — realization of the asserted facts in a world's history — is a separate claim, proved for the countermodel (diagTheory_prov_iff_recorded in Witness.lean, with soundness — not equivalence — at the truth layer: diagTheory_sound, true_but_unprovable); the two claims are stated separately and neither is presented as subsuming the other. Scope note: the adequacy requirement is de dicto (adequacy to the theory's observational consequences); a de re reading (reproducing the world's contingent outcome records) is a different demand, not one any limitative theorem they invoke addresses — see FIDELITY.md's closing section.

A4 (Deterministic process; measures as a degenerate case). D2 allows "computably sampleable measure." Our witness process is deterministic — the point-mass measure on its stream, which is trivially computably sampleable. Exhibiting one computable adequate process suffices for every existential claim we make; no claim quantifies over all simulations except P*-analysis, where the deterministic witness is what refutes P*.

A5 (Provability, not truth-in-the-standard-model, as the formal target). FKSM's Gödel and Chaitin prongs are provability-theoretic; the Tarski prong is about arithmetical truth. We formalize the decider that P* demands at the provability level (DecidesProv). FIDELITY.md addresses the truth-level reading: it is harder to decide truth than provability for the theories in question, so the non-existence half is a fortiori, and the simulation half (generation of observation streams) never mentions truth-sets, which is the point of T3.

A6 (The "world" of T2 is a dovetailing universal machine). T2's world is a universal machine world. We use mathlib's universal partial-recursive interpreter (Nat.Partrec.Code.eval, with its primitive-recursive time-bounded evaluator evaln) as the universal machine, and the world is the canonical dovetailer that runs every machine on every input. This is a universal machine in the literal technical sense; a specific universal CA (e.g. Rule 110) would add encoding overhead with no gain in content. The world's computability is machine-checked, not assumed.

A7 (What "the embedded prover derives Gödel" means formally — the honest split). Fully machine-checked: (i) the world is computable; (ii) it contains an embedded subsystem enumerating exactly the theorems of a concrete theory S₀ which is provably (in Lean) consistent, r.e., and incomplete; (iii) the Gödel–Rosser diagonal refutation is generated by the world itself: for every total computable candidate decider d of S₀-provability, there is a specific sentence σ_d on which d's verdict is contradicted by a certificate that appears in the world's own history, and the refutation ¬DecidesProv is drawn explicitly (theorems inside_refutation, inside_refutation_refutes). What remains prose: reading this as covering the FKSM evidence requires that the evidence they cite — the derivations of Gödel's, Tarski's, and Chaitin's theorems — consists of formal derivations: finite, checkable, r.e.-generable objects. That much is demonstrated rather than assumed (those proofs exist machine-checked; this repo itself machine-checks a Gödel–Rosser theorem, and formal derivations occur verbatim inside the computable world). Should someone instead locate the FKSM evidence in a non-formalizable insight over and above the derivations, it ceases to be intersubjective evidence and can no more support their premises than our refutation. Two further glosses declared as glosses: no observer or agent is formalized anywhere in the Lean development — "inhabitants" and "available to embedded observers" are interpretive readings of records in the world's history, and every epistemic-sounding claim reduces, on the machine-checked side, to the existence of such records; and "its own world's meta-theory" is licensed by reflexivity, not formalized semantics — DiagTheory's sentences assert halting facts about the very machines the world runs. Declared in VERIFICATION.md.

A8 (Toolchain pin). Lean 4.32.0 + mathlib v4.32.0 (latest stable pair at development time), with every transitive dependency pinned by exact commit in lean/lake-manifest.json; the required mathlib subset builds from source in about ten minutes if the binary cache is not used. MIT licensed (LICENSE, repository root).