The stage machine of the original Friedberg–Muchnik construction

This file constructs the finite-stage state machine of the original Friedberg–Muchnik theorem [S, VII.2.1], building two c.e. sets A = friedbergMuchnikSetA and B = friedbergMuchnikSetB against the interleaved negative requirements R_{2e} : A ≠ Φ_e^B and R_{2e+1} : B ≠ Φ_e^A.

At stage s, state s stores A_s, B_s, an active prefix of (witness, restraint) records, and a freshness floor floor; priorities beyond records.length default to (j.leastInPairColumn floor, none) (witness_restraint_eq_soareMarkers). The least priority k requiring attention enumerates witness k s into side k, protects monitoredSide k, installs some d.use at k, and resets all j > k above nextFloor.

References

• R. M. Friedberg, Two recursively enumerable sets of incomparable degrees of unsolvability, Proc. Nat. Acad. Sci. U.S.A. 43 (1957), 236–238.
• A. A. Muchnik, On the unsolvability of the problem of reducibility in the theory of algorithms, Dokl. Akad. Nauk SSSR 108 (1956), 194–197.
• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Theorem VII.2.1.

def TauCeti.FriedbergMuchnik.side (k : ℕ) : Bool

Side enumerated by requirement k: false (A) for 2e, true (B) for 2e + 1.

def TauCeti.FriedbergMuchnik.monitoredSide (k : ℕ) : Bool

Side monitored and protected by requirement k: the opposite side !k.bodd.

@[simp]

theorem TauCeti.FriedbergMuchnik.side_two_mul (e : ℕ) : side (2 * e) = false

Even priorities 2 * e enumerate into false (A).

@[simp]

theorem TauCeti.FriedbergMuchnik.side_two_mul_add_one (e : ℕ) : side (2 * e + 1) = true

Odd priorities 2 * e + 1 enumerate into true (B).

theorem TauCeti.FriedbergMuchnik.monitoredSide_eq_not_side (k : ℕ) : monitoredSide k = !side k

The monitored side is the negation of the enumerated side.

@[simp]

theorem TauCeti.FriedbergMuchnik.monitoredSide_two_mul (e : ℕ) : monitoredSide (2 * e) = true

Even priorities 2 * e monitor true (B).

@[simp]

theorem TauCeti.FriedbergMuchnik.monitoredSide_two_mul_add_one (e : ℕ) : monitoredSide (2 * e + 1) = false

Odd priorities 2 * e + 1 monitor false (A).

theorem TauCeti.FriedbergMuchnik.monitoredSide_ne_side (k : ℕ) : monitoredSide k ≠ side k

A requirement never monitors the side it enumerates into.

Finite active state and uniform column defaults

structure TauCeti.FriedbergMuchnik.State : Type

Finite state at the end of a stage: finite approximations setA and setB, active (witness, restraint) records for < records.length, and freshness floor floor.

• setA : Finset ℕ

  Current finite approximation to A (false).

• setB : Finset ℕ

  Current finite approximation to B (true).

• records : List (ℕ × Option ℕ)

  Active (witness, restraint) records indexed by priority.

• floor : ℕ

  Lower bound for default witness selection in j.pairColumn beyond records.length.

theorem TauCeti.FriedbergMuchnik.State.ext {x y : State} (setA : x.setA = y.setA) (setB : x.setB = y.setB) (records : x.records = y.records) (floor : x.floor = y.floor) : x = y

theorem TauCeti.FriedbergMuchnik.State.ext_iff {x y : State} : x = y ↔ x.setA = y.setA ∧ x.setB = y.setB ∧ x.records = y.records ∧ x.floor = y.floor

def TauCeti.FriedbergMuchnik.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TauCeti.FriedbergMuchnik.instDecidableEqState : DecidableEq State

def TauCeti.FriedbergMuchnik.State.init : State

The initial empty state at stage 0: empty sets, no active records, and floor 0.

def TauCeti.FriedbergMuchnik.State.set (st : State) : Bool → Finset ℕ

Select setA for false and setB for true.

@[simp]

theorem TauCeti.FriedbergMuchnik.State.set_false (st : State) : st.set false = st.setA

st.set false is st.setA.

@[simp]

theorem TauCeti.FriedbergMuchnik.State.set_true (st : State) : st.set true = st.setB

st.set true is st.setB.

def TauCeti.FriedbergMuchnik.State.witness (st : State) (j : ℕ) : ℕ

Witness of j in st (j.leastInPairColumn st.floor when st.records.length ≤ j).

theorem TauCeti.FriedbergMuchnik.State.witness_of_length_le {st : State} {j : ℕ} (hj : st.records.length ≤ j) : st.witness j = j.leastInPairColumn st.floor

Beyond st.records.length, st.witness j defaults to j.leastInPairColumn st.floor.

def TauCeti.FriedbergMuchnik.State.restraint (st : State) (j : ℕ) : Option ℕ

Restraint of j in st: recorded restraint if j < st.records.length, else none.

@[simp]

theorem TauCeti.FriedbergMuchnik.State.init_set (b : Bool) : init.set b = ∅

Both approximations in State.init are empty.

@[simp]

theorem TauCeti.FriedbergMuchnik.State.init_witness (j : ℕ) : init.witness j = Nat.pair 0 j

In State.init, requirement j holds the initial witness Nat.pair 0 j.

@[simp]

theorem TauCeti.FriedbergMuchnik.State.init_restraint (j : ℕ) : init.restraint j = none

In State.init, every restraint is inactive (none).

def TauCeti.FriedbergMuchnik.State.equivCode : State ≃ (ℕ × ℕ) × List (ℕ × Option ℕ) × ℕ

Equivalence between State and primitive-codable data via Finset.equivBitIndices.

@[instance_reducible]

instance TauCeti.FriedbergMuchnik.State.instPrimcodable : Primcodable State

Finite states are primitive codable via State.equivCode.

Stage evaluation, eligibility, and least-priority attention

def TauCeti.FriedbergMuchnik.stageRun (D : Finset ℕ) (s e x : ℕ) : Option Oracle.Single.Code.Halt

Normalized stage computation Φ_{e, s}^D(x) against the binary answers of a finite set D.

theorem TauCeti.FriedbergMuchnik.stageRun_def (D : Finset ℕ) (s e x : ℕ) : stageRun D s e x = Oracle.Single.Code.evalStage (fun (z : ℕ) => some (if z ∈ D then 1 else 0)) s (Denumerable.ofNat Oracle.Single.Code e) x

Unfolding stageRun.

theorem TauCeti.FriedbergMuchnik.stageRun_eq_evalStage_setAnswers (D : Finset ℕ) (s e x : ℕ) : stageRun D s e x = Oracle.Single.Code.evalStage (Oracle.Single.Code.setAnswers ↑D) s (Denumerable.ofNat Oracle.Single.Code e) x

stageRun agrees with Code.evalStage on Code.setAnswers D.

structure TauCeti.FriedbergMuchnik.RequiresAttention (st : State) (s k : ℕ) (d : Oracle.Single.Code.Halt) : Prop

k requires attention in st at stage s with halting record d when st.witness k lies in k.pairColumn \ st.set (side k) and Φ_{k / 2, s} halts there with output 0.

• witness_notMem : st.witness k ∉ st.set (side k)

  The witness has not yet entered the enumerated side of k.

• witness_mem_pairColumn : st.witness k ∈ k.pairColumn

  The witness belongs to k's column.

• stageRun_eq_some : stageRun (st.set (monitoredSide k)) s (k / 2) (st.witness k) = some d

  The opposite-oracle stage computation halts at the witness with record d.

• output_eq_zero : d.output = 0

  The stage computation outputs 0.

theorem TauCeti.FriedbergMuchnik.requiresAttention_iff {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} : RequiresAttention st s k d ↔ st.witness k ∉ st.set (side k) ∧ st.witness k ∈ k.pairColumn ∧ stageRun (st.set (monitoredSide k)) s (k / 2) (st.witness k) = some d ∧ d.output = 0

Unfolding RequiresAttention into its four clauses.

theorem TauCeti.FriedbergMuchnik.RequiresAttention.lt_stage {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : RequiresAttention st s k d) : k < s

Any requirement requiring attention at stage s has priority k < s.

theorem TauCeti.FriedbergMuchnik.RequiresAttention.unique {st : State} {s k : ℕ} {d d' : Oracle.Single.Code.Halt} (h : RequiresAttention st s k d) (h' : RequiresAttention st s k d') : d = d'

At fixed st, s, and k, the halting record witnessing RequiresAttention is unique.

def TauCeti.FriedbergMuchnik.attention (st : State) (s : ℕ) : Option (ℕ × Oracle.Single.Code.Halt)

Least-priority attention. Search k < s for the least priority requiring attention.

theorem TauCeti.FriedbergMuchnik.attention_eq_some_iff {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} : attention st s = some (k, d) ↔ RequiresAttention st s k d ∧ ∀ j < k, ∀ (d' : Oracle.Single.Code.Halt), ¬RequiresAttention st s j d'

attention st s = some (k, d) iff k is the least priority requiring attention at s.

theorem TauCeti.FriedbergMuchnik.attention_eq_none_iff {st : State} {s : ℕ} : attention st s = none ↔ ∀ (k : ℕ) (d : Oracle.Single.Code.Halt), ¬RequiresAttention st s k d

attention st s = none holds iff no priority requires attention.

@[simp]

theorem TauCeti.FriedbergMuchnik.attention_zero (st : State) : attention st 0 = none

No requirement can receive attention at stage 0.

Stage transition and semantic correspondence

def TauCeti.FriedbergMuchnik.nextFloor (st : State) (s k : ℕ) (d : Oracle.Single.Code.Halt) : ℕ

Freshness floor installed when k acts with d at stage s: strictly exceeds st.floor, s, d.use, st.setA ∪ st.setB, and all witnesses and active restraints of priority ≤ k.

theorem TauCeti.FriedbergMuchnik.lt_nextFloor_floor (st : State) (s k : ℕ) (d : Oracle.Single.Code.Halt) : st.floor < nextFloor st s k d

nextFloor strictly exceeds the previous floor st.floor.

theorem TauCeti.FriedbergMuchnik.lt_nextFloor_stage (st : State) (s k : ℕ) (d : Oracle.Single.Code.Halt) : s < nextFloor st s k d

nextFloor strictly exceeds the current stage s.

theorem TauCeti.FriedbergMuchnik.lt_nextFloor_use (st : State) (s k : ℕ) (d : Oracle.Single.Code.Halt) : d.use < nextFloor st s k d

nextFloor strictly exceeds the halting use d.use.

theorem TauCeti.FriedbergMuchnik.lt_nextFloor_of_mem_union {st : State} {s k x : ℕ} {d : Oracle.Single.Code.Halt} (hx : x ∈ st.setA ∪ st.setB) : x < nextFloor st s k d

nextFloor strictly exceeds every element already in st.setA ∪ st.setB.

theorem TauCeti.FriedbergMuchnik.witness_lt_nextFloor {st : State} {s k i : ℕ} {d : Oracle.Single.Code.Halt} (hi : i ≤ k) : st.witness i < nextFloor st s k d

nextFloor strictly exceeds st.witness i for every priority i ≤ k.

theorem TauCeti.FriedbergMuchnik.restraint_lt_nextFloor {st : State} {s k i b : ℕ} {d : Oracle.Single.Code.Halt} (hi : i ≤ k) (hb : st.restraint i = some b) : b < nextFloor st s k d

nextFloor strictly exceeds any active restraint st.restraint i = some b with i ≤ k.

def TauCeti.FriedbergMuchnik.step (st : State) (s : ℕ) : State

One step of the Friedberg–Muchnik stage machine.

def TauCeti.FriedbergMuchnik.state : ℕ → State

The finite state at the end of stage s.

def TauCeti.FriedbergMuchnik.action (s : ℕ) : Option ℕ

The priority receiving attention at stage s, if any.

def TauCeti.FriedbergMuchnik.stage (b : Bool) (s : ℕ) : Finset ℕ

Finite stage s of side b (A_s for false, B_s for true).

def TauCeti.FriedbergMuchnik.witness (j s : ℕ) : ℕ

Witness x_j^s of requirement j at stage s.

def TauCeti.FriedbergMuchnik.restraint (j s : ℕ) : Option ℕ

Restraint r_j^s of requirement j at stage s (none when inactive).

@[simp]

theorem TauCeti.FriedbergMuchnik.state_zero : state 0 = State.init

Stage 0 starts in State.init.

theorem TauCeti.FriedbergMuchnik.state_succ (s : ℕ) : state (s + 1) = step (state s) s

Stage s + 1 applies step to state s.

theorem TauCeti.FriedbergMuchnik.stage_def (b : Bool) (s : ℕ) : stage b s = (state s).set b

stage b s is (state s).set b.

theorem TauCeti.FriedbergMuchnik.witness_def (j s : ℕ) : witness j s = (state s).witness j

witness j s is (state s).witness j.

theorem TauCeti.FriedbergMuchnik.restraint_def (j s : ℕ) : restraint j s = (state s).restraint j

restraint j s is (state s).restraint j.

@[simp]

theorem TauCeti.FriedbergMuchnik.stage_zero (b : Bool) : stage b 0 = ∅

Both stage approximations start empty at stage 0.

@[simp]

theorem TauCeti.FriedbergMuchnik.witness_zero (j : ℕ) : witness j 0 = Nat.pair 0 j

At stage 0, requirement j holds the initial column witness Nat.pair 0 j.

@[simp]

theorem TauCeti.FriedbergMuchnik.restraint_zero (j : ℕ) : restraint j 0 = none

At stage 0, every restraint is inactive (none).

@[simp]

theorem TauCeti.FriedbergMuchnik.action_zero : action 0 = none

No requirement acts at stage 0.

theorem TauCeti.FriedbergMuchnik.action_eq_some_iff {s k : ℕ} : action s = some k ↔ ∃ (d : Oracle.Single.Code.Halt), attention (state s) s = some (k, d)

action s = some k iff attention (state s) s = some (k, d) for some halting record d.

theorem TauCeti.FriedbergMuchnik.action_eq_none_iff {s : ℕ} : action s = none ↔ attention (state s) s = none

action s = none iff attention (state s) s = none.

Action, locality, initialization, and opposite-oracle protection equations

@[simp]

theorem TauCeti.FriedbergMuchnik.step_of_attention_eq_none {st : State} {s : ℕ} (h : attention st s = none) : step st s = st

When no priority receives attention, step leaves st unchanged.

theorem TauCeti.FriedbergMuchnik.step_set_side_of_attention_eq_some {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) : (step st s).set (side k) = insert (st.witness k) (st.set (side k))

When k acts in st, step inserts st.witness k into (step st s).set (side k).

theorem TauCeti.FriedbergMuchnik.step_set_monitoredSide_of_attention_eq_some {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) : (step st s).set (monitoredSide k) = st.set (monitoredSide k)

When k acts in st, step leaves (step st s).set (monitoredSide k) unchanged.

theorem TauCeti.FriedbergMuchnik.step_records_of_attention_eq_some {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) : (step st s).records = List.map (fun (i : ℕ) => (st.witness i, st.restraint i)) (List.range k) ++ [(st.witness k, some d.use)]

Active records installed by step when k acts with d.

theorem TauCeti.FriedbergMuchnik.step_floor_of_attention_eq_some {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) : (step st s).floor = nextFloor st s k d

Freshness floor installed by step when k acts with d.

theorem TauCeti.FriedbergMuchnik.step_witness_of_attention_eq_some_of_le {st : State} {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) (hjk : j ≤ k) : (step st s).witness j = st.witness j

An action at k in st preserves witness j for j ≤ k.

theorem TauCeti.FriedbergMuchnik.step_witness_of_attention_eq_some_of_gt {st : State} {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) (hkj : k < j) : (step st s).witness j = j.leastInPairColumn (nextFloor st s k d)

An action at k in st resets witness j for j > k above nextFloor st s k d.

theorem TauCeti.FriedbergMuchnik.step_restraint_of_attention_eq_some_of_lt {st : State} {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) (hjk : j < k) : (step st s).restraint j = st.restraint j

An action at k in st preserves restraint j for j < k.

theorem TauCeti.FriedbergMuchnik.step_restraint_of_attention_eq_some_self {st : State} {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) : (step st s).restraint k = some d.use

An action at k with d in st activates restraint some d.use at k.

theorem TauCeti.FriedbergMuchnik.step_restraint_of_attention_eq_some_of_gt {st : State} {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention st s = some (k, d)) (hkj : k < j) : (step st s).restraint j = none

An action at k in st clears restraint j to none for j > k.

theorem TauCeti.FriedbergMuchnik.stage_succ_of_attention_eq_none {b : Bool} {s : ℕ} (h : attention (state s) s = none) : stage b (s + 1) = stage b s

If no requirement receives attention at stage s, stage b is unchanged.

theorem TauCeti.FriedbergMuchnik.stage_side_succ_of_attention_eq_some {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) : stage (side k) (s + 1) = insert (witness k s) (stage (side k) s)

An action of k enumerates witness k s into stage (side k).

theorem TauCeti.FriedbergMuchnik.witness_mem_stage_side_succ_of_attention_eq_some {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) : witness k s ∈ stage (side k) (s + 1)

When k acts at stage s, witness k s belongs to stage (side k) (s + 1).

theorem TauCeti.FriedbergMuchnik.stage_monitoredSide_succ_of_attention_eq_some {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) : stage (monitoredSide k) (s + 1) = stage (monitoredSide k) s

Protection of the opposite oracle. Action at k leaves stage (monitoredSide k) fixed.

theorem TauCeti.FriedbergMuchnik.witness_succ_of_attention_eq_none {j s : ℕ} (h : attention (state s) s = none) : witness j (s + 1) = witness j s

If no requirement receives attention at stage s, witness j is unchanged.

theorem TauCeti.FriedbergMuchnik.restraint_succ_of_attention_eq_none {j s : ℕ} (h : attention (state s) s = none) : restraint j (s + 1) = restraint j s

If no requirement receives attention at stage s, restraint j is unchanged.

theorem TauCeti.FriedbergMuchnik.witness_succ_of_attention_eq_some_of_le {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) (hjk : j ≤ k) : witness j (s + 1) = witness j s

Higher-priority witness locality. An action at k preserves witness j for j ≤ k.

theorem TauCeti.FriedbergMuchnik.restraint_succ_of_attention_eq_some_of_lt {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) (hjk : j < k) : restraint j (s + 1) = restraint j s

Higher-priority restraint locality. An action at k preserves restraint j for j < k.

theorem TauCeti.FriedbergMuchnik.restraint_succ_of_attention_eq_some_self {s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) : restraint k (s + 1) = some d.use

Self restraint activation. When k acts with d, restraint k (s + 1) = some d.use.

theorem TauCeti.FriedbergMuchnik.witness_succ_of_attention_eq_some_of_gt {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) (hkj : k < j) : witness j (s + 1) = j.leastInPairColumn (nextFloor (state s) s k d)

Lower-priority witness initialization. When k acts, j > k gets a fresh witness.

theorem TauCeti.FriedbergMuchnik.restraint_succ_of_attention_eq_some_of_gt {j s k : ℕ} {d : Oracle.Single.Code.Halt} (h : attention (state s) s = some (k, d)) (hkj : k < j) : restraint j (s + 1) = none

Lower-priority restraint initialization. When k acts, j > k has restraint none.

def TauCeti.FriedbergMuchnik.soareMarkers : ℕ → ℕ → ℕ × Option ℕ

Soare's infinite marker recurrence.

theorem TauCeti.FriedbergMuchnik.witness_restraint_eq_soareMarkers (s j : ℕ) : (witness j s, restraint j s) = soareMarkers s j

Semantic correspondence. (witness j s, restraint j s) agrees with soareMarkers s j.

Monotonicity, witness ownership, and appointment vs. attention

theorem TauCeti.FriedbergMuchnik.monotone_stage (b : Bool) : Monotone (stage b)

Both stage sequences stage false and stage true are monotone.

theorem TauCeti.FriedbergMuchnik.witness_mem_pairColumn (j s : ℕ) : witness j s ∈ j.pairColumn

Every witness witness j s belongs to j's pairing column j.pairColumn.

@[simp]

theorem TauCeti.FriedbergMuchnik.unpair_witness_snd (j s : ℕ) : (Nat.unpair (witness j s)).2 = j

The second Nat.unpair coordinate of witness j s is j.

theorem TauCeti.FriedbergMuchnik.requiresAttention_state_iff {s k : ℕ} {d : Oracle.Single.Code.Halt} : RequiresAttention (state s) s k d ↔ witness k s ∉ stage (side k) s ∧ stageRun (stage (monitoredSide k) s) s (k / 2) (witness k s) = some d ∧ d.output = 0

On a reachable state state s, RequiresAttention drops the automatic column clause.

theorem TauCeti.FriedbergMuchnik.monotone_witness (j : ℕ) : Monotone (witness j)

For each requirement j, the witness sequence s ↦ witness j s is monotone.

def TauCeti.FriedbergMuchnik.appointmentStages (j : ℕ) : Set ℕ

Stages at which j is appointed or reappointed a witness: 0 and initializationStages.

@[simp]

theorem TauCeti.FriedbergMuchnik.zero_mem_appointmentStages (j : ℕ) : 0 ∈ appointmentStages j

Stage 0 is an appointment stage for every requirement.

@[simp]

theorem TauCeti.FriedbergMuchnik.succ_mem_appointmentStages {j s : ℕ} : s + 1 ∈ appointmentStages j ↔ s + 1 ∈ Priority.initializationStages action j

A positive stage s + 1 is an appointment stage for j iff it initializes j.

theorem TauCeti.FriedbergMuchnik.disjoint_appointmentStages_attentionStages (j : ℕ) : Disjoint (appointmentStages j) (Priority.attentionStages action j)

Appointment and attention stages are disjoint.

theorem TauCeti.FriedbergMuchnik.witness_succ_eq_of_notMem_appointmentStages {j s : ℕ} (h : s + 1 ∉ appointmentStages j) : witness j (s + 1) = witness j s

Outside appointmentStages j, witness j does not change in s ↦ s + 1.

theorem TauCeti.FriedbergMuchnik.lt_nextFloor_of_mem_stage {b : Bool} {s k x : ℕ} {d : Oracle.Single.Code.Halt} (hx : x ∈ stage b s) : x < nextFloor (state s) s k d

nextFloor (state s) s k d strictly exceeds every element of stage b s.

theorem TauCeti.FriedbergMuchnik.witness_notMem_stage_of_mem_initializationStages {j s : ℕ} (b : Bool) (h : s + 1 ∈ Priority.initializationStages action j) : witness j (s + 1) ∉ stage b (s + 1)

At every reappointment stage s + 1 ∈ initializationStages action j, the new witness of j lies outside stage b (s + 1).

def TauCeti.FriedbergMuchnik.enumeratedBy (k : ℕ) : Set ℕ

Numbers enumerated by requirement k across all stages.

@[simp]

theorem TauCeti.FriedbergMuchnik.mem_enumeratedBy {k x : ℕ} : x ∈ enumeratedBy k ↔ ∃ (s : ℕ), action s = some k ∧ witness k s = x

Membership in enumeratedBy k.

theorem TauCeti.FriedbergMuchnik.enumeratedBy_subset_pairColumn (k : ℕ) : enumeratedBy k ⊆ k.pairColumn

Every number enumerated by requirement k belongs to k.pairColumn.

theorem TauCeti.FriedbergMuchnik.disjoint_enumeratedBy {j k : ℕ} (h : j ≠ k) : Disjoint (enumeratedBy j) (enumeratedBy k)

Distinct requirements enumerate disjoint sets of witnesses.

theorem TauCeti.FriedbergMuchnik.mem_fresh_stage {b : Bool} {s x : ℕ} : x ∈ Enumeration.fresh (stage b) s ↔ ∃ (k : ℕ), side k = b ∧ action s = some k ∧ witness k s = x

Fresh entries. x ∈ fresh (stage b) s iff the acting k has side k = b and witness k s = x.

Limit sets, disjointness, and effectivity

def TauCeti.FriedbergMuchnik.set (b : Bool) : Set ℕ

The limit set of side b: A for false and B for true.

def TauCeti.friedbergMuchnikSetA : Set ℕ

The first c.e. set A constructed by the original Friedberg–Muchnik theorem.

def TauCeti.friedbergMuchnikSetB : Set ℕ

The second c.e. set B constructed by the original Friedberg–Muchnik theorem.

theorem TauCeti.FriedbergMuchnik.set_eq_stageLimit (b : Bool) : set b = Enumeration.stageLimit (stage b)

set b is the stage limit stageLimit (stage b).

theorem TauCeti.FriedbergMuchnik.set_false_eq : set false = friedbergMuchnikSetA

set false is friedbergMuchnikSetA.

theorem TauCeti.FriedbergMuchnik.set_true_eq : set true = friedbergMuchnikSetB

set true is friedbergMuchnikSetB.

theorem TauCeti.FriedbergMuchnik.mem_set_iff_exists_stage {b : Bool} {x : ℕ} : x ∈ set b ↔ ∃ (s : ℕ), x ∈ stage b s

Membership in set b is eventual membership in stage b.

theorem TauCeti.FriedbergMuchnik.mem_set_iff_enumeratedBy {b : Bool} {x : ℕ} : x ∈ set b ↔ ∃ (k : ℕ), side k = b ∧ x ∈ enumeratedBy k

Witness ownership. x ∈ set b iff some k with side k = b enumerates x.

theorem TauCeti.FriedbergMuchnik.side_unpair_snd_of_mem_set {b : Bool} {x : ℕ} (hx : x ∈ set b) : side (Nat.unpair x).2 = b

Every element x ∈ set b has side x.unpair.2 = b.

theorem TauCeti.disjoint_friedbergMuchnikSetA_friedbergMuchnikSetB : Disjoint friedbergMuchnikSetA friedbergMuchnikSetB

friedbergMuchnikSetA and friedbergMuchnikSetB are disjoint.

theorem TauCeti.FriedbergMuchnik.primrec_attention : Primrec₂ attention

Least-priority attention selection is primitive recursive in the state and stage.

theorem TauCeti.FriedbergMuchnik.primrec_step : Primrec₂ step

The stage transition step is primitive recursive.

theorem TauCeti.FriedbergMuchnik.primrec_state : Primrec state

The finite state state s is primitive recursive in the stage s.

theorem TauCeti.FriedbergMuchnik.primrec_action : Primrec action

The acting priority action s is primitive recursive in the stage s.

theorem TauCeti.FriedbergMuchnik.primrec₂_witness : Primrec₂ witness

The witness witness j s is primitive recursive uniformly in (j, s).

theorem TauCeti.FriedbergMuchnik.primrec₂_restraint : Primrec₂ restraint

The restraint restraint j s is primitive recursive uniformly in (j, s).

theorem TauCeti.FriedbergMuchnik.primrec₂_stage : Primrec₂ fun (b : Bool) (s : ℕ) => Finset.equivBitIndices.symm (stage b s)

The binary finite-set codes of stage b s are primitive recursive uniformly in (b, s).

theorem TauCeti.FriedbergMuchnik.primrec_stage (b : Bool) : Primrec fun (s : ℕ) => Finset.equivBitIndices.symm (stage b s)

For each side b, the binary finite-set codes of stage b s are primitive recursive in s.

theorem TauCeti.FriedbergMuchnik.rePred_mem_set (b : Bool) : REPred fun (x : ℕ) => x ∈ set b

Both constructed limit sets set false and set true are c.e.

theorem TauCeti.rePred_mem_friedbergMuchnikSetA : REPred fun (x : ℕ) => x ∈ friedbergMuchnikSetA

friedbergMuchnikSetA is c.e.

theorem TauCeti.rePred_mem_friedbergMuchnikSetB : REPred fun (x : ℕ) => x ∈ friedbergMuchnikSetB

friedbergMuchnikSetB is c.e.