scripts/fill_logbook.py

"""Write the Trackio logbook pages (never via Write/Edit: the formatter hook mangles
embedded cell metadata)."""

import json
import os

ROOT = os.path.abspath(os.path.join(os.path.dirname(os.path.abspath(__file__)), ".."))
PAGES = os.path.join(ROOT, ".trackio", "logbook", "pages")


def cell(meta, body):
    return (
        "\n---\n<!-- trackio-cell\n"
        + json.dumps(meta)
        + "\n-->\n"
        + body.strip()
        + "\n"
    )


def write(slug, title, cells):
    d = os.path.join(PAGES, slug)
    os.makedirs(d, exist_ok=True)
    with open(os.path.join(d, "page.md"), "w") as f:
        f.write("# " + title + "\n" + "".join(cells))
    print("wrote", slug)


OUT = os.path.join(ROOT, "outputs")
poster = open(os.path.join(ROOT, "poster", "poster_embed.html")).read()

# ---------------------------------------------------------------- exec summary
EXEC = """
**Outcome: all six claims VERIFIED.** This is a constructive existence paper, so we reproduced
it by *building* the networks rather than re-reading the proof: an independent IEEE-754
floating-point network simulator with strictly left-to-right accumulation (cross-checked against
PyTorch autograd), plus our own construction of the paper's two gadgets. On a finite domain of
adjacent binary32 / binary64 numbers, a floating-point network simultaneously reproduces an
arbitrary target function `f*` **and** an arbitrary, independently drawn AD gradient `g*`
**bit for bit** -- max absolute error `0.0` on both, for ReLU, ELU, GELU, Swish, Sigmoid and
tanh, in binary32 and binary64, at every depth L = 5..12 (36 networks, 1188 value checks and 1188
gradient checks, zero mismatches). Lemma 3.4 (values kept, gradient identically 0) and Lemma 3.5
(output identically 0, gradient arbitrary) both reproduce exactly, and the mechanism claim is
confirmed three ways: re-running the *same* networks in exact rational arithmetic destroys both
constructions, deleting the +C/-C unit pair revives the suppressed gradient, and merely
*permuting the layer-1 unit order* -- a no-op in exact arithmetic -- does the same. The one
place we differ from the paper is in its favour but not in its wording: `L >= 9` is sufficient
but far from tight (our construction meets the same guarantee at `L = 5`; the authors' own
arXiv v2 lowers their bound to `L >= 7`).

## Scope & cost

| Item | Value |
| --- | --- |
| Scope | 6/6 claims; own simulator + own construction; 36 Theorem-3.1 networks, 12 Lemma-3.4, 12 Lemma-3.5, 16 depth variants, 1 Theorem-3.2 network; binary32 + binary64; exhaustive over every point of each finite domain |
| Hardware | CPU only (1 core), no GPU, no API key |
| Compute time | ~6 minutes wall clock total (largest single run: 4 min for the exhaustive binary16 sign-symmetry sweep over 4.03e9 ordered pairs) |
| Cost | $0 |
| Bit-exactness | every check is `==`, never a tolerance |
"""

write(
    "executive-summary",
    "Executive summary",
    [
        cell({"type": "markdown", "title": "Executive summary", "pinned": True}, EXEC),
        cell(
            {
                "type": "figure",
                "title": "Reproduction poster (poster_embed.html)",
                "pinned": True,
            },
            "````html\n" + poster.strip() + "\n````",
        ),
    ],
)

# ---------------------------------------------------------------- claim 1
C1 = """
### Claim (verbatim)

> Floating-point networks built from automatic differentiation can represent an arbitrary target
> floating-point function's values together with an arbitrary, independently chosen gradient on a
> bounded domain, using at least 9 layers (Theorem 3.1, Section 3).

**Verdict: VERIFIED.**

### Independent method

We did not transcribe the proof. We wrote (a) `scripts/fpnet.py`, an IEEE-754 sigma-network
simulator in which every scalar operation is a correctly-rounded machine operation and every
matrix-vector product is accumulated **strictly left to right**, exactly as the paper's
`D_{f,x}(g) = g (x) A_L (x) sigma'(y_{L-1}) (x) ... (x) sigma'(y_1) (x) A_1` requires; and (b)
`scripts/construct.py`, our own construction of `f = f2 # f1`. All activation operating points
are *searched numerically* per activation and per format, never assumed from the paper.

The simulator was cross-checked against **PyTorch autograd** on random networks
(`scripts/check_torch.py`): max relative gradient difference `7.5e-7` (binary32) and `4.0e-15`
(binary64) -- the residue is PyTorch's own summation order, which is exactly the phenomenon the
paper is about.

### Scale, seeds, domain

* Domain `X` = 33 points, every other binary32 number of `[1,2)` (spacing 2 ulp) -- i.e. adjacent
  floating-point numbers, the densest finite domain that exists; the binary64 runs use the
  analogous grid.
* Targets `f*`, `h*`, `g*` drawn independently at random (seeds 20260725, ...+1, ...+2), with the
  theorem's only hypothesis enforced (`h*(x) = 0 => g*(x) = 0`, ~15% of points).
* Depth `L = 9` for the headline runs; the check is run at **every** point of `X`, not a sample.

### Numerical result

| quantity | value |
| --- | --- |
| networks built | 36 (6 activations x 2 formats x 3 seeds) |
| value checks | 1188, **1188 exact** |
| gradient checks | 1188, **1188 exact** |
| max abs error, `f(x) - f*(x)` | **0.0** |
| max abs error, `D_{f,x}(h*(x)) - g*(x)` | **0.0** |
| 2-D domain (6x6 grid, d = 2) | 0 mismatches, both components of `g*` exact |

Expected value: exact equality, since the theorem is an existence statement about exact
floating-point equality -- and that is what we get.

### Boundary / counterexample audit

* **Depth sweep.** `L = 5, 6, 7, 8, 9, 10, 11, 12` -- all exact (`outputs/claim1_depth.json`).
  The claim's `L >= 9` is therefore **sufficient and true**, but it is *not tight*: our
  independent construction achieves the same guarantee at **`L = 5`**, and the authors' own
  arXiv v2 (Theorem 1) lowers their bound to `L >= 7`. This is a non-tightness finding, not a
  contradiction: the theorem says "for any `L >= 9` there exists an `L`-layer network", which
  holds.
* **Genuine lower bound.** `L = 1` (a bare affine map) gives `D_{f,x}(y) = y (x) A_1`, which does
  not depend on `x` at all; we confirm numerically that the gradient is constant across `x`. So
  *some* depth is genuinely required and the claim is not vacuous.
* **Domain extent.** The paper's Theorem 1 domain is `[-2^125, 2^125]_F`. Ours is smaller: our
  construction's internal annihilating constants overflow beyond `|x| ~ 2^36` (ReLU/ELU),
  `2^44` (GELU/Swish), `2^20` (Sigmoid/tanh) in binary32 (`outputs/claim1_wide_domain.json`).
  The claim as stated ("on a bounded domain") is verified; we did **not** reproduce the paper's
  full domain extent with our own construction, and say so.

### Limitation

The construction uses one parallel branch per domain point, so `|X|` is the network width. The
paper's domain `[-2^125, 2^125]_F` contains ~2^127 points and is unbuildable by anyone, including
the authors; every implementation (theirs and ours) verifies on a finite subset. Theorem 3.5/5,
the general-activation version, explicitly covers any sigma-distinguishable `X`, so a finite grid
is inside the theorem's stated scope.

### Artifacts

`scripts/fpnet.py`, `scripts/construct.py`, `scripts/run_claims.py`,
`outputs/claim12_theorem31.json`, `outputs/claim1_multidim.json`,
`outputs/claim1_depth.json`, `outputs/claim1_wide_domain.json`,
`outputs/torch_crosscheck.json`, `figs/fig2_exactness.png`.
"""
write(
    "claim-1-thm-3-1-values-independent-gradient-9-layers",
    "Claim 1: Thm 3.1: values + independent gradient, >=9 layers",
    [cell({"type": "markdown", "title": "Claim 1 - Theorem 3.1"}, C1)],
)

# ---------------------------------------------------------------- claim 2
C2 = """
### Claim (verbatim)

> This representability result is established for the practical activation functions ReLU, ELU,
> GELU, Swish, Sigmoid, and tanh (Theorem 3.1, Section 3).

**Verdict: VERIFIED (all six, both formats).**

### Independent method

The same Theorem-3.1 construction is instantiated for each sigma. Crucially, the construction is
**not** the same for all six: which mechanism suppresses the gradient is decided by the
activation, and our implementation discovers that automatically by searching each activation's
operating points numerically (`acfg()` in `scripts/construct.py`):

* **ReLU, ELU, GELU, Swish** -- there is no point where `sigma' = 0` while `sigma != 0`, so the
  gradient must be annihilated inside the AD accumulation by a `+C / -C` unit pair.
* **Sigmoid, tanh** -- these saturate: `sigma = +-1` *exactly* while the rounded derivative
  `sigma'` has already **underflowed to exactly 0**. The value survives and the gradient does
  not, with no pair needed. This is precisely the paper's Condition 1 regime
  `|sigma'(gamma)| <= 2^{-k}|sigma(gamma)|`.

The operating scales found numerically (smallest power of two at which the required exactness
holds) are, for binary32 / binary64: ReLU 1/1, ELU 2/2, GELU 16/32, Swish 64/1024,
Sigmoid 128/1024, tanh 32/512.

### Numerical result

Every one of the 12 (activation x format) cells: **0 value mismatches and 0 gradient
mismatches** over 33 domain points x 3 seeds, max abs error `0.0`. Identical outcome for
Lemma 3.4 and Lemma 3.5 alone (12 more networks each).

| sigma | binary32 | binary64 |
| --- | --- | --- |
| ReLU | 0 / 99 mismatches | 0 / 99 |
| ELU | 0 / 99 | 0 / 99 |
| GELU | 0 / 99 | 0 / 99 |
| Swish | 0 / 99 | 0 / 99 |
| Sigmoid | 0 / 99 | 0 / 99 |
| tanh | 0 / 99 | 0 / 99 |

### Boundary / sensitivity audit

* **Derivative convention.** The paper defines `sigma' = round(sigma_hat')`, the rounded *true*
  derivative. PyTorch instead computes sigmoid/tanh backward from the *output*
  (`out * (1 - out)`), which underflows to 0 even earlier. We implement the paper's convention as
  primary and ship the framework convention (`ACTS_FRAMEWORK` in `scripts/fpnet.py`); the
  framework convention makes gradient suppression strictly *easier*, so the claim is robust to
  the choice.
* **Saturating activations need an even grid.** For Sigmoid/tanh our detector uses two threshold
  knots that must fall strictly between domain points and stay exactly representable; the domain
  is therefore every *other* float rather than every float. This is a property of our
  construction, not of the theorem.

### Limitation

GELU is evaluated with the exact erf form (`t * Phi(t)`), not the tanh approximation used by some
frameworks; Swish uses beta = 1. Both are the standard definitions and are stated in the code.

### Artifacts

`scripts/construct.py` (function `acfg`), `outputs/claim12_theorem31.json`,
`outputs/claim4_lemma34.json`, `outputs/claim5_lemma35.json`, `figs/fig2_exactness.png`.
"""
write(
    "claim-2-thm-3-1-holds-for-relu-elu-gelu-swish-sigmoid-tanh",
    "Claim 2: Thm 3.1: holds for ReLU/ELU/GELU/Swish/Sigmoid/tanh",
    [cell({"type": "markdown", "title": "Claim 2 - six activations"}, C2)],
)

# ---------------------------------------------------------------- claim 3
C3 = """
### Claim (verbatim)

> A single floating-point network can produce a gradient that varies with the loss function's
> derivative, provided that derivative satisfies an antisymmetry condition g*(x,-y) = -g*(x,y)
> (Theorem 3.2, Section 3).

**Verdict: VERIFIED** for both halves of the statement, at reduced scale on the second half
(see Limitation -- we state the shortfall explicitly rather than claiming full coverage).

### Half A -- the antisymmetry condition is NECESSARY (exhaustive)

The paper says the restriction "cannot be bypassed due to the symmetry inherent in the definition
of `D^AD`". We turned that into an executable, exhaustive statement. IEEE-754 multiplication and
addition are exactly sign-symmetric, `fl(-a*b) = -fl(a*b)` and `fl(-a-b) = -fl(a+b)`, so for
*every* floating-point network and every `x`, `D_{f,x}(-y) = -D_{f,x}(y)` identically. Any target
`g*` violating `g*(x,-y) = -g*(x,y)` is therefore unrepresentable -- a *falsification* result for
the complementary claim.

| check | scale | violations |
| --- | --- | --- |
| `fl(-a*b) == -fl(a*b)` over binary16 | all 63,488 finite values, **4,030,726,144 ordered pairs** | **0** |
| `fl((-a)+(-b)) == -fl(a+b)` over binary16 | same 4.03e9 pairs | **0** |
| `D_{f,x}(-y) == -D_{f,x}(y)` on random binary32 nets | 200 networks x 8 input gradients = 1600 pairs, all six activations | **0** |

### Half B -- a single network whose gradient genuinely varies with y

Under exact real arithmetic the chain rule forces
`grad(phi o f)(x) = phi'(f(x)) * grad f(x)`, i.e. the AD gradient is *exactly proportional* to
`y = phi'_x(f(x))`. We built one floating-point network (3 layers, 72 units, ReLU, binary32) with

* `f(x) = 0` for every `x` (its forward accumulation is annihilated by a `+C/-C` constant pair);
* `D_{f,x}(y)` **prescribed to arbitrary, independently drawn antisymmetric values on 24
  magnitude bands of `y`**.

Each band is a chain `((y (x) p_j) (x) w) (x) a_j` whose second product **underflows to exactly
zero** below the band threshold, so a band contributes nothing until `|y|` crosses it.

| quantity | value |
| --- | --- |
| bands (and their negatives) | 24, i.e. 48 prescribed values |
| exact hits | **48 / 48** |
| `f(x)` on all probes | **0 everywhere** |
| spread of `|D_{f,x}(y) / y|` across the tested range | **8.47 orders of magnitude** |
| same graph in exact rational arithmetic | ratio `D/y` **constant** (2.582e-17 at every `y`) |

The last row is the decisive contrast: the identical computational graph is exactly proportional
to `y` in exact arithmetic and wildly non-proportional in IEEE-754.

### Limitation (stated, not softened)

Theorem 3.2 asks for arbitrary antisymmetric `g*(x,y)` for **all** `y in [-H,H]_F`. We verify
arbitrary `g*` on a **24-band finite subset** of `y` (48 values with signs), not on all 2^32
binary32 values. The paper's full-range construction needs `L >= 2^{E+1} + 2M + 11 = 569` layers
in binary32; we did not build it. What we *did* establish at full scale is Half A (exhaustive)
and the existence of non-proportional dependence with prescribed values.

### Artifacts

`scripts/run_thm32.py`, `outputs/claim3_theorem32.json`, `figs/fig4_thm32.png`.
"""
write(
    "claim-3-thm-3-2-gradient-varies-with-phi-prime-under-antisymmetry",
    "Claim 3: Thm 3.2: gradient varies with phi-prime under antisymmetry",
    [cell({"type": "markdown", "title": "Claim 3 - Theorem 3.2"}, C3)],
)

# ---------------------------------------------------------------- claim 4
C4 = """
### Claim (verbatim)

> Lemma 3.4 constructs networks that represent the correct function values while completely
> suppressing the computed gradient to zero (Lemma 3.4, Section 3.3).

**Verdict: VERIFIED.**

### Independent method

`mode="lem34"` of our construction: a 9-layer sigma-network with `f(x) = f*(x)` for all `x` in a
finite domain and `D_{f,x}(y) = 0` for **every** input gradient `y`, not just for one. For
ReLU/ELU/GELU/Swish the suppression is a `+C/-C` unit pair placed *after* the value path inside
the AD accumulation `grad(x_k) = (+)_r s_r (x) A_1[r,k]`: the two units are identical and their
downstream weights are `+w, -w`, so the forward pass cancels them exactly and never sees them,
while the backward accumulation is annihilated by `(t (+) C) (-) C = 0`. For Sigmoid/tanh the
rounded derivative has already underflowed to 0 where sigma is exactly `+-1`, and no pair is
needed.

### Scale and result

12 networks (6 activations x 2 formats), 17 domain points each, and a sweep of input gradients
`y = +-2^e` covering the whole exponent range (46 values for binary32, 276 for binary64) plus
`0` and `Omega`.

| quantity | value |
| --- | --- |
| value mismatches | **0** in every configuration (max abs error `0.0`) |
| gradient exactly zero | for all `|y|` up to the per-activation bound below |

### Boundary audit -- where it degrades, and how

The suppression is exact until the annihilating constant `C` would overflow, at which point the
gradient leaks. This is a real, quantified boundary (`outputs/claim4_lemma34.json`):

| sigma | binary32: largest `|y|` still exactly suppressed | first `|y|` that leaks |
| --- | --- | --- |
| ReLU, ELU | `2.31e18` (2^61) | `5.90e20` |
| GELU, Swish | `9.90e27` (2^93) | `9.90e27` |
| Sigmoid | `1.66e35` (2^117) | `4.25e37` |
| tanh | `2.54e30` (2^101) | `6.49e32` |

In binary64 the same pattern holds with the bounds at `5.3e269` (ReLU/ELU) up to `2.7e303`
(Sigmoid). Values remain bit-exact on both sides of the boundary -- only the gradient leaks.
This mirrors the paper's own `H_sigma` bookkeeping (the input gradient must be bounded), though
our numeric bound is a property of *our* construction, not of the paper's.

### Limitation

Our per-activation `|y|` ceiling is lower than the paper's `H_sigma = Omega` for the ReLU family;
the paper's construction budgets overflow more carefully (its Conditions 1-3 exist for exactly
this reason). We report our achieved range rather than claiming theirs.

### Artifacts

`scripts/construct.py` (`mode="lem34"`), `scripts/run_claims.py`,
`outputs/claim4_lemma34.json`, `figs/fig3_lemma34_range.png`.
"""
write(
    "claim-4-lemma-3-4-correct-values-gradient-suppressed-to-zero",
    "Claim 4: Lemma 3.4: correct values, gradient suppressed to zero",
    [cell({"type": "markdown", "title": "Claim 4 - Lemma 3.4"}, C4)],
)

# ---------------------------------------------------------------- claim 5
C5 = """
### Claim (verbatim)

> Lemma 3.5 constructs networks that output zero everywhere while still producing an arbitrary
> target gradient under automatic differentiation (Lemma 3.5, Section 3.3).

**Verdict: VERIFIED.**

### Independent method

`mode="lem35"`: the dual gadget. The forward value is annihilated by a `+C/-C` constant pair
*inside a forward accumulation* -- the AD pass never meets that pair, because the backward pass
*multiplies* along that edge instead of summing. The target gradient is then synthesised by
"carrier" units in layer 1 whose weights are solved for exactly by a residual refinement
(`_calibrate_carriers`), and gated on `x = z_i` by a unit whose `sigma'` is exactly 0 off its own
point.

### Scale and result

12 networks (6 activations x 2 formats), 9 layers, 17 domain points each, with `g*` drawn at
random (`|g*|` up to 235.7) and `h*` including zeros.

| check | result |
| --- | --- |
| `f(x) = 0` exactly on every domain point | **204 / 204** |
| `f(x) = 0` exactly on 64 off-grid probes per network | **768 / 768** |
| `D_{f,x}(h*(x)) = g*(x)` bit-exact | **204 / 204** |
| max abs error, values and gradients | **0.0** |

### Why this is the sharp form of the paper's warning

A network that outputs identically zero looks completely inert in any forward test -- and hands
an attacker-chosen gradient to whatever consumes it (a PINN residual, an adversarial-example
loop, an input-optimisation attack). The forward pass carries no signal that the gradient has
been chosen.

### Boundary audit

Concatenating this network with any other of the same depth leaves the other network's forward
value untouched (the pair resets the accumulator to exactly 0 and later summands are added
afterwards), which is the third conclusion of the lemma (`(f # f~)(x) = f~(x)`) and is what makes
`f = f2 # f1` work for Theorem 3.1 -- verified implicitly by every Theorem 3.1 run.

### Limitation

Same finite-domain limitation as Claim 1: `|X|` parallel branches. Off-grid inputs are probed
(and give exactly 0) but the *gradient* is only specified on `X`, as in the lemma.

### Artifacts

`scripts/construct.py` (`mode="lem35"`), `outputs/claim5_lemma35.json`.
"""
write(
    "claim-5-lemma-3-5-zero-output-arbitrary-ad-gradient",
    "Claim 5: Lemma 3.5: zero output, arbitrary AD gradient",
    [cell({"type": "markdown", "title": "Claim 5 - Lemma 3.5"}, C5)],
)

# ---------------------------------------------------------------- claim 6
C6 = """
### Claim (verbatim)

> The construction exploits the non-associativity of floating-point arithmetic to decouple the
> computed gradient from the classical chain-rule proportionality that would hold under exact
> real arithmetic (Section 1.1).

**Verdict: VERIFIED**, by three independent tests, one of which is a direct falsification of the
exact-arithmetic alternative.

### Test 1 -- the identity, at the magnitudes actually used

`(t (+) C) (-) C = 0` while `t (+) (C (-) C) = t`, i.e. the same three numbers give different
answers under different association:

| `t` | `C` | left-assoc `(t+C)-C` | right-assoc `t+(C-C)` |
| --- | --- | --- | --- |
| 1.21e-9 | 1.0 | **0.0** | 1.21e-9 |
| 1.27e-3 | 1.05e6 | **0.0** | 1.27e-3 |
| 1.40e9 | 1.15e18 | **0.0** | 1.40e9 |
| 1.53e21 | 1.27e30 | **0.0** | 1.53e21 |

### Test 2 -- exact rational arithmetic destroys both constructions

We re-ran the *same* ReLU networks -- identical weights, identical graph -- with Python
`fractions.Fraction`, i.e. no rounding anywhere (`FPNet.forward_exact` / `backward_exact`).

| network | IEEE-754 | exact rationals |
| --- | --- | --- |
| Lemma 3.4: `max |D_{f,x}(y)|` (target 0) | **0** | **3.60e9** |
| Lemma 3.5: `max |f(x)|` (target 0) | **0** | **2.88e17** |

Both gadgets collapse the moment rounding is removed: the suppressed gradient comes back, and the
zeroed output comes back. The effect is the rounding itself, not an artefact of our simulator.

### Test 3 -- two ablations

* **Delete the `+C/-C` pair** (set its output weight to 0, changing nothing else): the values stay
  bit-exact and the AD gradient jumps from `0` to `7.73e9`.
* **Permute the layer-1 unit order** so the pair sits *before* the value path instead of after.
  Same weights, same graph, same function in exact arithmetic -- only the summation order of the
  AD accumulation changes. The gradient again jumps to `7.73e9` while `f` remains bit-exact.

The permutation ablation is the cleanest possible statement of the paper's Section 1.1: the AD
gradient is a property of the **order of operations**, not of the function.

### What would have falsified this

A gradient that survived the pair; a value the pair disturbed; an exact-arithmetic run that agreed
with the floating-point one; a permutation that left the gradient unchanged. We tested for all
four and found none.

### Limitation

The exact-arithmetic contrast is run for ReLU only, because ReLU is the one activation in the set
whose exact real form is rational (so `Fraction` can represent the whole network without
approximation). For the other five the same argument holds structurally but cannot be evaluated
in exact rational arithmetic.

### Artifacts

`scripts/run_claims.py` (`exp_mechanism`), `scripts/fpnet.py`
(`forward_exact` / `backward_exact`), `outputs/claim6_mechanism.json`,
`figs/fig1_mechanism.png`.
"""
write(
    "claim-6-mechanism-fp-non-associativity-decouples-ad-gradient",
    "Claim 6: Mechanism: FP non-associativity decouples AD gradient",
    [cell({"type": "markdown", "title": "Claim 6 - non-associativity"}, C6)],
)

# ---------------------------------------------------------------- conclusion
BUNDLE = """
## Reproduction bundle & rerun

The bundle contains every script, every raw result JSON and every figure of this reproduction.

```
scripts/fpnet.py        IEEE-754 sigma-network + left-to-right AD simulator, exact-rational reference
scripts/construct.py    our own construction of f = f2 # f1 (Lemma 3.4 / 3.5 / Theorem 3.1)
scripts/run_claims.py   claims 1, 2, 4, 5, 6
scripts/run_thm32.py    claim 3 (exhaustive antisymmetry + y-dependent gradient)
scripts/run_domain.py   domain-extent boundary sweep
scripts/check_torch.py  cross-check of the simulator against PyTorch autograd
scripts/make_figs.py    figures
outputs/*.json          raw results (one file per claim)
figs/*.png              figures
poster/                 poster.html (posterly GATE PASS), preview PDF/PNG, poster_embed.html
paper/                  arXiv v1 + v2 text, and the authors' released code (yechanp/fp-grad-rep)
```

```bash
pip install numpy scipy matplotlib torch     # CPU only
python scripts/check_torch.py                # simulator vs PyTorch autograd
python scripts/run_claims.py all             # claims 1, 2, 4, 5, 6   (~2 min)
python scripts/run_thm32.py                  # claim 3               (~4 min)
python scripts/run_domain.py                 # domain boundary sweep
python scripts/make_figs.py                  # figures
```

Every check in `run_claims.py` and `run_thm32.py` is bit-exact equality; a run that prints
non-zero mismatch counts is a failed reproduction.

**Verdict summary**

| claim | verdict | key number |
| --- | --- | --- |
| 1 - Thm 3.1, values + independent gradient, `L >= 9` | verified | 1188/1188 value and 1188/1188 gradient checks exact, max abs error `0.0` |
| 2 - holds for ReLU/ELU/GELU/Swish/Sigmoid/tanh | verified | 12/12 activation x format cells, 0 mismatches |
| 3 - Thm 3.2, gradient varies with `phi'` under antisymmetry | verified (reduced-scale on the second half) | 0 antisymmetry violations in 4.03e9 exhaustive binary16 pairs; 48/48 prescribed gradients exact; `|D/y|` spans 8.47 decades |
| 4 - Lemma 3.4, values kept, gradient suppressed | verified | gradient exactly 0 for every `y` up to `2^61` (ReLU) .. `2^117` (Sigmoid), values always exact |
| 5 - Lemma 3.5, zero output, arbitrary gradient | verified | 204/204 gradients exact, 972/972 outputs exactly 0 |
| 6 - non-associativity is the mechanism | verified | exact-rational rerun: suppressed gradient returns at `3.6e9`, zeroed output at `2.9e17` |

**Where we differ from the paper.** Nothing contradicts it. Two honest deltas: (i) `L >= 9` is
sufficient but not tight -- our construction reaches the same guarantee at `L = 5` and the
authors' arXiv v2 lowers their own bound to `L >= 7`; (ii) our construction's usable domain and
input-gradient range are narrower than the paper's `M_sigma`/`H_sigma`, because we did not
replicate their overflow bookkeeping.

Paper: [arXiv 2605.01702](https://arxiv.org/abs/2605.01702) *
[OpenReview g89qqA6qmD](https://openreview.net/forum?id=g89qqA6qmD) *
authors' code: [yechanp/fp-grad-rep](https://github.com/yechanp/fp-grad-rep) (ReLU only; we did
not reuse it -- it is vendored under `paper/official_code/` for reference).
"""
write(
    "conclusion",
    "Conclusion",
    [
        cell(
            {
                "type": "artifact",
                "title": "Reproduction bundle",
                "artifact_type": "dataset",
            },
            "fpnet-ad-repro/repro-bundle:v0",
        ),
        cell({"type": "markdown", "title": "Download & rerun"}, BUNDLE),
    ],
)
print("done")