Paper-fragment ↔ finite-field bridge #
FieldEmbedding.agreeBy (Nock/ModularEval.lean) identifies the full evaluators — evalN
(unbounded Nat increment) and evalFBy q (modular increment, main.tex:1531–1534) — conditional
on a successful run of the guarded evaluator evalGBy q, which crashes rather than letting any
increment reach q. But all three of those evaluators include OP₁₁, while
- the small-step machine
Verb.runProgramand its unconditional adequacy partnerevalPaper(Verb.runProgram_adequate_complete), and - the strict modular paper oracle
evalPaperMod q(Nock/PaperReferenceMod.lean)
live in the paper's OP₀–OP₁₀ fragment (main.tex:1054–1076).
This module supplies the guarded paper-fragment evaluator evalGPaper q (evalPaperMod q with the
crashing increment lusGBy q) and threads one conditional through every layer, ending in
paper_field_bridge: on q-bounded inputs, a successful guarded fragment run makes the small-step
machine, evalPaper, evalPaperMod q, evalFBy q, and evalN all return the same noun, itself
q-bounded.
The conditional is no-overflow; injectivity is the payoff, not a second hypothesis: the BoundedBy q
conclusion makes the leaf cast ℕ → ZMod q injective (embBy_inj_of_boundedBy), so the structural
noun equality used by OP₅ (main.tex:1525) is field equality on bridged results. Primality is
never used — 1 < q suffices — so nothing here declares or pulls a project axiom.
The conditional is STRICTLY STRONGER than the paper's own total modular language: evalGPaper q
crashes where the paper's modular OP₄ merely wraps, so this identifies the five evaluators on the
no-overflow sublanguage only (evalGPaper_fails_where_evalPaperMod_wraps).
The guarded paper-fragment evaluator #
*[subject formula], fuel-indexed, guarded paper fragment: the paper's OP₀–OP₁₀ fragment
with the OP₄ increment lusGBy q, which crashes rather than reaching an atom ≥ q.
evalGPaper q fuel s f = some r is therefore exactly the statement "this paper-fragment
computation runs without any OP₄ modular wrap at q" — the honest no-overflow side
condition, in the fragment where Verb.runProgram and evalPaperMod q live. (OP₄ is the only
opcode these evaluators reduce with a modular increment; see the OP₆ note below.)
OP₆ NOTE. These modular evaluators reduce OP₆ by the standard Nock loobean if/else on the
condition (main.tex:1067 computes the same thing over ℕ via an increment macro). Over ℕ they
coincide (runProgram_adequate_complete), and under the bridge's BoundedBy q hypotheses for
q ≥ 4 every intermediate atom is < q so no OP₆ increment could wrap either; hence the guard
is complete on the bridge's domain. The paper's literal OP₆ macro, whose two increments are
modular, diverges from the if/else only for an unbounded (≥ q) or small-modulus (q ∈ {2,3})
condition — inputs outside the bounded domain — so paper_field_bridge is unaffected at
q ≥ 4. This is a representation choice (if/else vs increment-macro), documented, not an
OP₄-style wrap.
Equations
- One or more equations did not get rendered due to their size.
- Nock.evalGPaper q 0 x✝¹ x✝ = none
- Nock.evalGPaper q n.succ x✝ (Nock.Noun.atom a) = none
- Nock.evalGPaper q fuel.succ x✝ ((b.cell c).cell d) = match Nock.evalGPaper q fuel x✝ (b.cell c), Nock.evalGPaper q fuel x✝ d with | some l, some r => some (l.cell r) | x, x_1 => none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 0).cell (Nock.Noun.atom ax)) = Nock.Noun.slot ax x✝
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 0).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 1).cell tail) = some tail
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 2).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 3).cell tail) = Option.map Nock.Noun.wut (Nock.evalGPaper q fuel x✝ tail)
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 4).cell tail) = (Nock.evalGPaper q fuel x✝ tail).bind (Nock.FieldEmbedding.lusGBy q)
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 5).cell (b.cell c)) = match Nock.evalGPaper q fuel x✝ b, Nock.evalGPaper q fuel x✝ c with | some sb, some sc => some (sb.tis sc) | x, x_1 => none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 5).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 6).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 7).cell (b.cell c)) = match Nock.evalGPaper q fuel x✝ b with | some sb => Nock.evalGPaper q fuel sb c | none => none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 7).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 8).cell (b.cell c)) = match Nock.evalGPaper q fuel x✝ b with | some sb => Nock.evalGPaper q fuel (sb.cell x✝) c | none => none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 8).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 9).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom 10).cell tail) = none
- Nock.evalGPaper q fuel.succ x✝ ((Nock.Noun.atom op).cell tail) = none
Instances For
The increment agrees under the guard #
The guard is the only place the three fragment evaluators can differ: a successful lusGBy q
pins n + 1 < q, and there the unbounded increment Noun.lus and the modular increment
lusFBy q produce the same atom.
A successful guarded increment is the unbounded increment (main.tex:1531–1534 vs Noun.lus).
A successful guarded increment is the paper's modular increment (main.tex:1531–1534).
The three refinements out of the guarded fragment #
evalGPaper q refines evalGBy q. The guarded fragment run is a guarded full run with
the same value; they differ only where evalGBy fires OP₁₁, which the fragment crashes on.
This is what makes FieldEmbedding.agreeBy reusable inside the fragment.
evalGPaper q refines evalPaper. Under the guard the fragment's modular-range OP₄ and
the unbounded Nat OP₄ coincide, so a successful guarded run is a evalPaper run with the same
value — the entry point into the unconditional runProgram ↔ evalPaper adequacy.
evalGPaper q refines evalPaperMod q. A successful guarded run is a strict-paper
modular run with the same value: the guard rules out the wrap that is the only difference.
The injectivity carry #
BoundedBy q is precisely the condition under which the leaf cast ℕ → ZMod q is injective, so on
bridged results the structural noun equality used by OP₅ (main.tex:1525) coincides with equality
of field images. Injectivity is thus a consequence of the bridge's conclusion, not an extra
hypothesis. These do not use any project axiom.
embBy q is injective on q-bounded nouns. Distinct canonical residues < q stay
distinct in ZMod q, so structural Nock equality is field equality there (main.tex:1525).
The capstone bridge #
Paper ↔ finite-field bridge. On q-bounded inputs (every atom is a canonical residue
< q), a successful guarded paper-fragment run makes all five formalizations of the paper's
evaluation agree on one noun, which is again q-bounded:
- the small-step machine
Verb.runProgram(main.tex:1052–1083), - the Nat paper oracle
evalPaper, - the strict modular paper oracle
evalPaperMod q(main.tex:1531–1534), - the full modular evaluator
FieldEmbedding.evalFBy q, and - the Nat reference
evalN.
The single hypothesis evalGPaper q fuel s f = some r is no-overflow: it is discharged by
running the guarded evaluator, not assumed. The BoundedBy q r conclusion then delivers
leaf-cast injectivity for free (bridge_reflects_field_equality).
The bridge's small-step half in the form the machine consumes.
The bridge's field half: a successful guarded fragment run is a full modular run.
The bridge carries the equivalence through the field embedding. Two guarded fragment runs
on q-bounded inputs whose results have the same field image have the same result noun: the
no-overflow conditional yields boundedness, and boundedness yields injectivity.
Non-vacuity, and the guard cuts exactly at the wrap #
The witnesses instantiate the full six-fold bridge conclusion at a genuine prime and at the paper's
own characteristic (main.tex:158), given as a literal modulus so no primality axiom is needed
(the bridge never uses primality).
The Goldilocks modulus p = 2^64 − 2^32 + 1 (main.tex:158), as a literal Nat constant.
Used only to instantiate a bridge witness at the paper's own characteristic; primality is not
assumed anywhere.
Instances For
Non-vacuity at a genuine prime. *[0 [4 [1 3]]] = 4 at q = 5, where ZMod q really is a
field, with the full six-fold bridge conclusion.
Non-vacuity at the paper's own characteristic goldilocksModulus = 2^64 − 2^32 + 1.
Uses the literal modulus; no primality axiom.
The guard rejects exactly the divergent computation. At the top residue q−1 = 4 the
strict modular oracle wraps to 0 while the unbounded oracle produces 5
(evalPaperMod_ne_evalPaper_at_top); the guarded fragment evaluator crashes there, so the
bridge never claims agreement across the wrap.
One residue below the top the guard holds and all three fragment oracles agree.