pith. machine review for the scientific record. sign in
theorem proved term proof high

simulation_hypothesis_structure

show as:
view Lean formalization →

The theorem asserts that the simulation hypothesis structure holds in Recognition Science by equating it to the Church-Turing physics structure derived from the ledger. Researchers analyzing Bostrom-style simulation arguments or information-theoretic foundations of physics would cite this result when showing that RS dissolves rather than refutes the hypothesis. The proof is a one-line wrapper applying the has_ct_structure theorem.

claimThe proposition that Church-Turing physics follows from the ledger holds.

background

The module treats the ledger as the sole physical substrate, with no external computer or separate reality possible. Existence is governed by the J-cost: an entity x with x > 0 exists precisely when J-cost(x) = 0, which forces x = 1. The upstream has_ct_structure theorem establishes that Church-Turing physics follows from the ledger, and the simulation hypothesis from ledger is defined as exactly that proposition.

proof idea

The proof is a one-line wrapper that applies the has_ct_structure theorem, which itself reduces directly to the church_turing_physics_structure result.

why it matters in Recognition Science

This result completes the IC-004 series by confirming the simulation hypothesis structure, supporting the module's dissolution of the simulation argument: the ledger is self-grounded and any simulation of it is again a ledger. It aligns with the Recognition Science view that the ledger satisfies the it-from-bit requirement trivially. No open scaffolding remains here.

scope and limits

formal statement (Lean)

 136theorem simulation_hypothesis_structure : simulation_hypothesis_from_ledger :=

proof body

Term-mode proof.

 137  has_ct_structure
 138
 139/-- Church-Turing physics implies simulation-hypothesis structure. -/

depends on (2)

Lean names referenced from this declaration's body.