Information Church Turing Physics Structure Finite Function Is Computable

The computability of finite functions

In mathematics, a function is a rule that assigns to each input exactly one output. When both the set of possible inputs and the set of possible outputs are finite, the function can always be described by a finite table: a list of input-output pairs. The theorem finite_function_is_computable states this precisely: for any function f from a finite type α to a finite type β, there exists a finite set of pairs (a, b) such that for every input a, the pair (a, f a) is in the set. This is a purely mathematical statement, true for any finite sets, and it is proved in the framework's machine-checked library of formal theorems.

The statement is elementary, but it carries weight in the Recognition Science framework. The framework models physical dynamics as a ledger, a discrete record of events. The ledger's state at any moment is a finite object: a function from eight phases to a boolean value, giving 2^8 = 256 possible states. A transition from one state to the next is therefore a function from a finite set to itself. The theorem guarantees that any such transition can be represented by a finite table, which is exactly what a Turing machine can process. This is the bridge from the framework's discrete structure to the claim that its dynamics are computable.

The framework uses this to argue for a version of the Church-Turing thesis applied to physics: any process it describes can be simulated by a Turing machine. The argument is that the ledger updates in discrete ticks, each tick updates a finite number of entries, and each transition is a finite function, hence computable. The framework also notes that this does not imply all real numbers are exactly computable: the golden ratio, which appears in the framework's cost function, is not a rational number, so it cannot be exactly represented by a finite computation, only approximated to any desired precision.

What the theorem does not claim is more important than what it does. It does not claim that the framework's physical model is correct, or that the ledger structure is how nature actually works. It does not claim that every physical process in the real world is computable; that is a separate, empirical question. It does not claim that the halting problem is decidable for the framework's dynamics; in fact, the framework states that the halting problem for its dynamics inherits undecidability from Turing machines. The theorem is a mathematical fact about finite functions, and the framework uses it as one step in a larger argument, not as a proof of the physical thesis by itself.

/-- **THEOREM IC-003.10**: Every finite function on a finite type is "computable"
    in the sense that it can be represented by a lookup table. -/
theorem finite_function_is_computable {α β : Type*} [Fintype α] [Fintype β]
    [DecidableEq α] [DecidableEq β]
    (f : α → β) :
    ∃ (table : Finset (α × β)),
      ∀ a : α, ∃ b : β, (a, b) ∈ table ∧ f a = b := by
  use Finset.image (fun a => (a, f a)) Finset.univ
  intro a
  exact ⟨f a, Finset.mem_image.mpr ⟨a, Finset.mem_univ a, rfl⟩, rfl⟩

/-- **THEOREM IC-003.4**: The discrete ledger state space is finite (exactly 2^8 = 256). -/
theorem ledger_state_space_finite :
    Fintype.card DiscreteLedgerState = 2 ^ 8 := by
  simp [DiscreteLedgerState, Fintype.card_pi, Fintype.card_fin, Fintype.card_bool]

/-- **THEOREM IC-003.3**: Any ledger transition on the 8-tick phase space is
    a function on a finite type, hence computable by table lookup.
    Since there are only 2^8 = 256 possible discrete ledger states, any
    transition function can be pre-computed as a finite lookup table. -/
theorem discrete_ledger_computable (t : LedgerTransition) :
    ∃ (table : Finset (DiscreteLedgerState × DiscreteLedgerState)),
      ∀ (s : DiscreteLedgerState),
        ∃ (s' : DiscreteLedgerState), (s, s') ∈ table ∧ t s = s' := by
  use Finset.image (fun s => (s, t s)) Finset.univ
  intro s
  exact ⟨t s, Finset.mem_image.mpr ⟨s, Finset.mem_univ s, rfl⟩, rfl⟩

/-- **THEOREM IC-003.12**: φ is irrational, so RS dynamics involving φ-ladders
    cannot be exactly computed by finite rational algorithms.
    This places exact RS computations in the class of "real number computations"
    (beyond classical Turing machines for exact values). -/
theorem rs_dynamics_beyond_rational : ¬ ∃ q : ℚ, (q : ℝ) = phi :=
  fun ⟨q, hq⟩ => no_exact_phi_computation q hq

/-- The Church-Turing physics property: physical processes are computable. -/
def church_turing_physics_from_ledger : Prop := computation_limits_from_ledger

What this page does not claim

The theorem does not prove that the framework's physical model is correct. The theorem does not claim that all real physical processes are computable. The theorem does not claim that the halting problem for the framework's dynamics is decidable.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/ChurchTuringPhysicsStructure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: