Completeness for the derived OP₀–OP₁₀ oracle

progressP and the denotation-keyed vcost/pcost measure show every successful evalPaper evaluation is realized by runProgram.

Helper: right child of a denP-defined editOk node is denP-defined at the SAME fuel

theorem Nock.Verb.denP_right_F {a : Action} {l r : Verb} {f : ℕ} {x : Noun} (hok : (node a l r).editOk = true) (h : denP (f + 1) (node a l r) = some x) : ∃ (yr : Noun), denP (f + 1) r = some yr

theorem Nock.Verb.denP_children_F {a : Action} {l r : Verb} {F : ℕ} {x : Noun} (hok : (node a l r).editOk = true) (h : denP F (node a l r) = some x) : (∃ (yl : Noun), denP F l = some yl) ∧ ∃ (yr : Noun), denP F r = some yr

theorem Nock.Verb.isTerminal_node {a : Action} {l r : Verb} : (node a l r).isTerminal = (a.isNull && l.isTerminal && r.isTerminal)

theorem Nock.Verb.denP_terminal_val {v : Verb} {F : ℕ} {y : Noun} (ht : v.isTerminal = true) (h : denP F v = some y) : y = v.noun

theorem Nock.Verb.denP_term_children {a : Action} {l r : Verb} {F : ℕ} {x : Noun} (hok : (node a l r).editOk = true) (h : denP F (node a l r) = some x) (htl : l.isTerminal = true) (htr : r.isTerminal = true) : denP F l = some l.noun ∧ denP F r = some r.noun

theorem Nock.Verb.denP_term_split {l r : Verb} {f : ℕ} {x : Noun} (htl : l.isTerminal = true) (htr : r.isTerminal = true) (h : denP (f + 1) (node Action.null l r) = some x) : denP f l = some l.noun ∧ denP f r = some r.noun

theorem Nock.Verb.denP_star_val {A B : Verb} {f : ℕ} {a b w : Noun} (hA : denP f A = some a) (hB : denP f B = some b) (he : evalPaper f a b = some w) : denP (f + 1) (node Action.star A B) = some w

theorem Nock.Verb.denP_null_val {A B : Verb} {f : ℕ} {a b : Noun} (hA : denP f A = some a) (hB : denP f B = some b) : denP (f + 1) (node Action.null A B) = some (a.cell b)

theorem Nock.Verb.denP_null_none {A B : Verb} {f : ℕ} (hA : denP f A = none) : denP (f + 1) (node Action.null A B) = none

theorem Nock.Verb.isTerminal_of_map_ofNoun {o : Option Noun} {r₀ : Verb} (h : Option.map ofNoun o = some r₀) : r₀.isTerminal = true

theorem Nock.Verb.pcost_align {n m k : ℕ} {a b r : Noun} (h : evalPaper n a b = some r) (hm : n ≤ m) (hk : n ≤ k) : pcost m a b = pcost k a b

Controlled vcost node equations (avoid simp [vcost] over-unfolding literals)

theorem Nock.Verb.vcost_star_eq {F : ℕ} {l r : Verb} : vcost F (node Action.star l r) = (match denP F l, denP F r with | some sa, some fo => pcost F sa fo | x, x_1 => 0) + vcost F l + vcost F r

theorem Nock.Verb.vcost_slot_eq {F : ℕ} {l r : Verb} : vcost F (node Action.slot l r) = 1 + vcost F l + vcost F r

theorem Nock.Verb.vcost_equal_eq {F : ℕ} {l r : Verb} : vcost F (node Action.equal l r) = 1 + vcost F l + vcost F r

theorem Nock.Verb.vcost_minus_eq {F : ℕ} {l r : Verb} : vcost F (node Action.minus l r) = 1 + vcost F l + vcost F r

theorem Nock.Verb.vcost_edit_eq {F : ℕ} {l r : Verb} : vcost F (node Action.edit l r) = 1 + vcost F l + vcost F r

theorem Nock.Verb.vcost_null_eq {F : ℕ} {l r : Verb} : vcost F (node Action.null l r) = vcost F l + vcost F r

theorem Nock.Verb.vcost_wut_eq {F : ℕ} {l r : Verb} : vcost F (node Action.wut l r) = vcost F l + vcost F r

theorem Nock.Verb.vcost_star_terminal {F : ℕ} {A B : Verb} (hA : A.isTerminal = true) (hB : B.isTerminal = true) (hdA : denP F A = some A.noun) (hdB : denP F B = some B.noun) : vcost F (node Action.star A B) = pcost F A.noun B.noun

vcost of a *-node with terminal, denP-defined children is the firing pcost.

Lemma 1 — vcost_succ

theorem Nock.Verb.vcost_succ {F : ℕ} {v : Verb} {x : Noun} (hok : v.editOk = true) (hv : denP F v = some x) : vcost (F + 1) v = vcost F v

Lemma 2 — vcost_mono

theorem Nock.Verb.vcost_mono {F G : ℕ} {v : Verb} {x : Noun} (hle : F ≤ G) (hok : v.editOk = true) (hv : denP F v = some x) : vcost G v = vcost F v

theorem Nock.Verb.EvP_det {a b y1 y2 : Noun} (h1 : EvP a b y1) (h2 : EvP a b y2) : y1 = y2

theorem Nock.Verb.denP_null_leaf0 {inner : Verb} {f : ℕ} {dv : Noun} (h : denP (f + 1) (node Action.null (leaf 0) inner) = some dv) : ∃ (w : Noun), dv = (Noun.atom 0).cell w

theorem Nock.Verb.op6_decrease {g : ℕ} {L b thn els : Verb} {x : Noun} {rn2 rc : Action} (hL : L.isTerminal = true) (htc : (node rc thn els).isTerminal = true) (hthn : thn.isTerminal = true) (htels : els.isTerminal = true) (hgc : denP g (node rc thn els) = some (node rc thn els).noun) (hdL : denP (g + 1 + 1) L = some L.noun) (h4b : denP (g + 1 + 1) (node Action.null (leaf 4) (node Action.null (leaf 4) b)) = some ((Noun.atom 4).cell ((Noun.atom 4).cell b.noun))) (ht4 : (node Action.null (leaf 4) (node Action.null (leaf 4) b)).isTerminal = true) (ht23 : (node Action.null (leaf 2) (leaf 3)).isTerminal = true) (hvv : evalPaper (g + 1) L.noun ((Noun.atom 6).cell (node rn2 b (node rc thn els)).noun) = some x) : vcost (g + 1 + 1) (node Action.star L (node Action.star (node rc thn els) (node Action.null (leaf 0) (node Action.star (node Action.null (leaf 2) (leaf 3)) (node Action.null (leaf 0) (node Action.star L (node Action.null (leaf 4) (node Action.null (leaf 4) b)))))))) < pcost (g + 1 + 1) L.noun (node Action.null (leaf 6) (node rn2 b (node rc thn els))).noun

OP₆ strict local decrease (if-then-else macro). The reduct is a 6-level nested *-tree; its vcost is SF(L,a0) + SF(c,b0) + SF([2,3],d0) + SF(L,[4[4b]]), where the last is exactly 4 + pcost g L b, the middle two are ≤ 2 (op0), and the first is 0 or the branch cost (matching the RHS branch by a full evaluation trace b → *[L,b]∈{0,1} → +2 → slot → branch). The op₆ weight 100 dominates the macro skeleton (8).

Lemma 3 — cost_local (strict local decrease at a *-redex)

theorem Nock.Verb.cost_local {F : ℕ} {L R rr : Verb} {x : Noun} (hL : L.isTerminal = true) (hR : R.isTerminal = true) (hv : denP F (node Action.star L R) = some x) (hr : (node Action.star L R).reduce = some rr) : vcost F rr < vcost F (node Action.star L R)

Lemma 4 — step congruence and cost_stepP

theorem Nock.Verb.enum_denP_F {F : ℕ} (v : Verb) : v.editOk = true → ∀ (c : ℕ) (x : Noun), denP F v = some x → ∀ p ∈ (v.enum c).2, ∃ (y : Noun), denP F p.2 = some y

theorem Nock.Verb.denP_F_subnode {F : ℕ} {v : Verb} {x : Noun} (hok : v.editOk = true) (hv : denP F v = some x) {i : ℕ} {sub : Verb} (hmap : map i v = some sub) : ∃ (y : Noun), denP F sub = some y

theorem Nock.Verb.replaceAux_notMem (i : ℕ) (r₀ v : Verb) (c : ℕ) : findAt i (v.enum c).2 = none → (replaceAux i r₀ v c).2 = v

theorem Nock.Verb.denP_F_swap_eq {F : ℕ} {w w' : Verb} (hok : w.editOk = true) (hrel : w.RelP w') {a b : Noun} (ha : denP F w = some a) (hb : denP F w' = some b) : a = b

theorem Nock.Verb.vcost_replace_cong (F i : ℕ) (sub r₀ : Verb) (hpend : sub.isPending = true) (hgraph : ∀ (y : Noun), sub.DenP y ↔ r₀.DenP y) (hr0 : r₀.editOk = true) (v : Verb) (c : ℕ) (xv xv' : Noun) : v.editOk = true → findAt i (v.enum c).2 = some sub → denP F v = some xv → denP F (replaceAux i r₀ v c).2 = some xv' → vcost F (replaceAux i r₀ v c).2 + vcost F sub = vcost F v + vcost F r₀

Step congruence for vcost. Swapping the (denotation-preserving, pending) subnode sub for r₀ changes vcost F by exactly vcost F r₀ - vcost F sub (additive form).

theorem Nock.Verb.cost_stepP {F : ℕ} {v v' : Verb} {x x' : Noun} (hwf : v.editOk = true) (hv : denP F v = some x) (hv' : denP F v' = some x') (h : v.next = some v') : vcost F v' < vcost F v

A single machine step strictly decreases vcost (at a common fuel F).

Lemma 5 — run_completeP

theorem Nock.Verb.run_completeP {v : Verb} {x : Noun} (hok : v.editOk = true) (hv : v.DenP x) : ∃ (N : ℕ), run N v = some x

Lemma 6 — paperComplete_holds

theorem Nock.Verb.paperComplete_holds : PaperComplete

OP₀–OP₁₀ consistency

theorem Nock.Verb.runProgram_adequate_complete (s f r : Noun) : (∃ (fuel : ℕ), runProgram fuel s f = some r) ↔ ∃ (fuel : ℕ), evalPaper fuel s f = some r

The paper-derived local machine and derived OP₀–OP₁₀ oracle compute the same partial function. This is a Lean consistency theorem, not a theorem stated in main.tex.