Figure 7Schematic restoration pipeline on (3,5,6) to (3,4,6)
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
Generated from paper_jmlr.tex, lines 1476–1490.
2 Explain this
Read the top row left to right, then the bottom row right to left. The boxes group algorithmic operations, not individual gates or layers. The candidate tests run in parallel. Additional heaps enlarge the circuit's width; the first-candidate selection uses a parallel priority encoder rather than a sequential search over heaps.
Two-frame restoration, step by step
Exact construction trace Every value is computed from the construction’s definitions for the example shown.
This is the checked two-frame selector run on one example, gate group by gate group. It starts from the two frames of Figure 2 and ends with the binary output fields shown in Figure 7. Every value below is computed from the selector's definition for the boards shown. Choose another example to see several candidates at once, the fallback, or a terminal board. The two examples marked "outside the promise" do not start from a zero-nim-sum board after a legal move, so the guarantee does not apply to them.
Inside the promise. The earlier board has nim-sum 0 and the opponent decreased one heap, so the restoration theorem guarantees that the output restores nim-sum 0.
Compare the frames bit by bit
Each heap is a 3-bit block. For every heap and every bit position, one two-input XOR compares Q with Q′, all in parallel.
Heap Q Q′ XOR Heap 0 3 011 3 011 000 same 1 5 101 4 100 001 changed 2 6 110 6 110 000 same Extract the difference δ
Bit k of δ is the OR of column k of the XOR table: 001 = δ = 1.
At most one heap changed, so at most one row is nonzero and the OR equals the XOR of the rows, which is nim(Q) ⊕ nim(Q′).
Propose replacements and test them in parallel
For every heap at once: replace Q′i by Q′i ⊕ δ and test whether that is a decrease. The decisive bit is the highest set bit of δ (weight 1): a heap passes exactly when it has that bit set.
Heap Q′ Q′ ⊕ δ Test 0 3 011 2 010 passes: 2 < 3 1 4 100 5 101 fails: 5 > 4 2 6 110 7 111 fails: 7 > 6 Show the bit comparisons
The test x ⊕ δ < x is a fixed-depth circuit: an OR over the possible highest differing bit, requiring equality above it, a 1 in x and a 0 in the replacement at that bit.
- Heap 0: 011 vs 010 — the highest differing bit has weight 1; the heap has 1 there, so the replacement is smaller.
- Heap 1: 100 vs 101 — the highest differing bit has weight 1; the heap has 0 there, so the replacement is larger.
- Heap 2: 110 vs 111 — the highest differing bit has weight 1; the heap has 0 there, so the replacement is larger.
Candidates passing: 1.
Choose between cancelling and the fallback
cancelling move At least one replacement passes, so the flags are the passing tests and the fallback is masked off.
Heap passes nonzero fallback value flag si 0 1 1 3 − 1 = 2 1 1 0 1 4 − 1 = 3 0 2 0 1 6 − 1 = 5 0 Encode the first flagged heap as a binary index
For N = 3 heaps the construction uses r = ⌊log2 N⌋ + 1 = 2 index bits (the encoder itself needs only N ≤ 2r). The first flag is at heap 0, so the index bits are 00.
Show the priority encoder
fi = si ∧ ¬sj for all j < i keeps only the first flag; index bit k is the OR of fi over the heaps i whose binary index has a 1 at bit k. This is a fixed-depth circuit, not a search.
Heap i i in binary si first fi 0 00 1 1 1 01 0 0 2 10 0 0 Index bits (OR of the fi in each 1-column): 00
Output the move
validity1index (2 bits)00value (3 bits)010
Decoded move: set heap 0 to 2. New board (2, 4, 6), nim-sum 0.
How this relates to the Lean proof. The selector is Family.restS (B, N): the local difference circuits
LocalRestore.dC, the candidate tests of SelectCircuit.varSel and the priority encoder PriorityEncoder.encode,
read on the two-frame input LocalRestore.tf. Family.rest_semantics proves that, on the promised
domain, these formulas and the compiled network output a legal move that restores nim-sum 0. Outside the promise the
circuit still computes the values shown, and no theorem says that the result restores 0.
What this does not show. The selector does not find a first winning move from an arbitrary board. Given a zero-nim-sum predecessor it maintains the invariant (Theorem 5.12(iii)). The boxes of Figure 7 group operations; the stages here group gates, not network layers.
3 How this is formalised
This is a schematic of the checked restoration construction, specialised to the numerical example in Section C, “From a game rule to a network”. It omits the general fallback and terminal branches for readability. The full statements are available through Appendix C, “Local differences and candidate moves” and Appendix C, “A binary index is part of the circuit”.
| Paper anchor | fig:construction-pipeline (manuscript label) |
|---|---|
| Displayed as | Figure 7 |
| Claim | Schematic restoration pipeline on (3,5,6) to (3,4,6) |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1476–1490; SHA-256 of the normalised block source 907077765feb76ad… |
| Depends on | Section C, “From a game rule to a network”, Appendix C, “Local differences and candidate moves”, Appendix C, “A binary index is part of the circuit” |
| Explanations | explain/fig:construction-pipeline, formal/fig:construction-pipeline |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).