Documentation

LeanPool.PureNock.PaperReferenceMod

Strict modular paper oracle #

evalPaperMod q: the paper's OP₀–OP₁₀ fragment (main.tex:1054–1076) over Nat-atom nouns, with the OP₄ increment taken modulo q, exactly as the paper specifies +(n) = (1+n) mod p (main.tex:1531–1534).

It is the strict-language counterpart of evalPaper:

Two facts must not be conflated:

  1. evalPaperMod q refines the full modular evaluator FieldEmbedding.evalFBy q (evalPaperMod_le_evalFBy): they agree on the whole OP₀–OP₁₀ fragment and differ only where evalFBy would fire OP₁₁, which the paper fragment crashes on.
  2. evalPaperMod q is not evalPaper: at the top atom q−1 the modular OP₄ wraps to 0 while the unbounded evalPaper produces q (evalPaperMod_ne_evalPaper_at_top). This is the compiled no-overflow distinction, not a claim that the two coincide.
source
def Nock.evalPaperMod (q : ℕ) :
ℕ → Noun → Noun → Option Noun

*[subject formula], fuel-indexed, strict paper fragment (OP₀–OP₁₀ + cons) with the paper's modular OP₄ increment +(n) = (1+n) mod q (main.tex:1531–1534).

Identical to FieldEmbedding.evalFBy q except an OP₁₁ head (op = 11) is an unknown opcode and crashes (none), matching the paper's opHeadOk (op < 11) and the small-step machine runProgram.

Equations
Instances For
    source
    def Nock.evalPaperModTop (q : ℕ) (subj formula : Noun) :
    Option Noun

    Convenience wrapper with a large fuel budget, for #eval sanity checks.

    Equations
    Instances For
      source
      theorem Nock.evalPaperMod_succ {q n : ℕ} {s form r : Noun} (h : evalPaperMod q n s form = some r) :
      evalPaperMod q (n + 1) s form = some r

      Fuel monotonicity (single step) for evalPaperMod.

      source
      theorem Nock.evalPaperMod_mono {q n m : ℕ} {s form r : Noun} (hle : n ≤ m) (h : evalPaperMod q n s form = some r) :
      evalPaperMod q m s form = some r

      Fuel monotonicity for evalPaperMod.

      source
      theorem Nock.evalPaperMod_le_evalFBy {q n : ℕ} {s form r : Noun} (h : evalPaperMod q n s form = some r) :
      FieldEmbedding.evalFBy q n s form = some r

      evalPaperMod q refines evalFBy q. Every strict-paper modular evaluation is a full modular evaluation with the same result: they differ only where evalFBy fires OP₁₁, which evalPaperMod crashes on.

      source
      theorem Nock.evalPaperMod_boundedBy {q fuel : ℕ} {s f r : Noun} (hq : 1 < q) (hs : FieldEmbedding.BoundedBy q s) (hf : FieldEmbedding.BoundedBy q f) (h : evalPaperMod q fuel s f = some r) :
      FieldEmbedding.BoundedBy q r

      evalPaperMod q preserves q-boundedness (unconditionally). On canonical field-noun inputs (BoundedBy q), every successful modular run returns a canonical field noun — the modular oracle maps 𝒩(𝔽) into 𝒩(𝔽), handling the wrap exactly (no guard needed).

      source
      theorem Nock.evalPaperMod_ne_evalPaper_at_top :
      evalPaperMod 3 5 (Noun.atom 0) ((Noun.atom 4).cell ((Noun.atom 1).cell (Noun.atom 2))) ≠ evalPaper 5 (Noun.atom 0) ((Noun.atom 4).cell ((Noun.atom 1).cell (Noun.atom 2)))

      Modular OP₄ differs from the unbounded increment at the top atom. On +(2) at q = 3 the modular oracle wraps ((2+1) mod 3 = 0) while the unbounded evalPaper produces 3. This is the compiled distinction: the strict paper language is the modular one, not the unbounded evalPaper.