High-Stakes Generality · Algorithmic Approximation · 2026-06-30

Cheaper to check than to find. Machine-checked across seven problems.

A public Lean ledger machine-checks a single “cheap CHECK” statement across seven instances — max-flow / min-cut, König matching / cover, 2-SAT decision, Pratt primality, shortest-path, syndrome verifier, and ReLU gate-count — under one Certifies interface. The find-side of every instance stays imported. Alongside, the tropical / piecewise-linear core compiles cancellation-free circuits exactly (ε = 0) to ReLU networks at linear gate count ≤ 4N via a sharing-aware DAG (compileToDag) — the ε = 0 piecewise-linear core for arXiv:2606.26705 Thm 3.2 / Cor 5.1. The N-1 monotone-depth-as-computation theorem closes the lower bound in the cancellation-free model: the tent's 2^d expressivity requires cancellation, while monotone depth is region-polynomial. Public, reproducible, axiom-clean (no sorry, no native_decide, no trusted compiler step).

find/check ledger · 7 instances DAG linear gate count · ≤ 4N N-1 fully closed · cancellation-free is region-polynomial universal approximation · constructive, axiom-clean N-2 synthesis · typed-conjecture organizing read N-4 empirical · 0.89 with named SGD residual axiom-clean · AxiomAudit-gated

Claim boundary — read this first

This page is method context for a Lean ledger about checking. It is not a P-vs-NP advance and not a complexity-theoretic separation. The lane borrows the find-vs-check asymmetry as vocabulary. Hardness is imported in every instance — decoding hardness, depth-vs-width lower bounds, factoring, Cook-Levin — Lean certifies the deductive CHECK side only.

Pratt is NP-membership (a short certificate exists that a checker verifies fast); it is not a fast primality test, and finding the witness still requires factoring p−1. The find/check modules CHECK a supplied optimum; they are not solvers. N-1 is a lower bound in the cancellation-free fragment; the general depth-vs-width lower bound (Telgarsky / Eldan-Shamir) stays imported. N-2's “every wall is cancellation” reading is a typed conjecture, machine-checked only on the fold / monotone / region axes. N-4 is an empirical finding: region geometry predicts the generalization threshold modulo SGD trainability — no theorem, no guarantee. “Lean-verified” applies to the deductive cores, never to the imported hardness or to the whole story.

The find/check ledger — Certifies with seven instances

Seven CHECK-side theorems under one interface.

Each row plugs into the shared ledger via a Certifies.Ledger instance with an O(·) cheap-CHECK theorem; the find-side stays imported. The reusable core is weakDuality_tight: weak duality (every primal ≤ every dual) plus a tight pair (p = d) implies both optima at once (IsGreatest P p ∧ IsLeast D d) — axiom-free, the purest certificate core.

Instance	Kind	What is checked (Lean)	Find-side (imported)
max-flow / min-cut `MaxFlowMinCut`	combinatorial LP-dual optimization	`weak_duality`: `value F ≤ capCut cap S` (skew-symmetric within-cut cancellation, conservation collapses the `S`-sum to source net out-flow, across-cut bounded by capacity). `maxflow_mincut`: tight pair via `weakDuality_tight`.	finding the actual max-flow algorithm (Edmonds-Karp, push-relabel, Dinic's): not formalized; the cert checks a supplied flow / cut pair.
König matching / cover `MatchingCover`	combinatorial LP-dual optimization	`matching_le_cover`: every vertex cover upper-bounds every matching, via an injection matched-edge → cover-endpoint. `konig`: tight pair via `weakDuality_tight`.	finding the max matching or the min cover: not formalized; cert checks a supplied pair.
2-SAT decision `TwoSat`	decision / NP-verification	`check_correct`: the `O(\|φ\|)` evaluator decides the language. `cert_sound`: a satisfying assignment certifies satisfiability. Axiom-light: `[propext, Quot.sound]`; the eval is decidable.	finding the satisfying assignment via the implication-graph SCC algorithm: not formalized; cert checks a supplied assignment.
Pratt primality `PrattCert`	number theory / NP-membership	`prime_iff_witness`: a primitive-root `Witness` certifies primality. `cert_sound` / `cert_complete` wrap mathlib's `lucas_primality` / `reverse_lucas_primality`.	finding the witness requires factoring `p−1`: not a fast primality test; cert checks a supplied witness.
shortest-path `ShortestPathCert`	combinatorial LP-dual feasibility	`feasible_le_walk`: any feasible dual lower-bounds the shortest walk. `cert_isLeast`: exact optimality at the tight pair.	finding the shortest path (Dijkstra, Bellman-Ford): not formalized as an algorithm; cert checks a supplied dual.
syndrome verifier `Certificate` / `CheckCost`	finite-field algebra / coding	syndrome-certificate soundness + exact algebraic lossiness + reject-bound behavior + check-cost scaling `verifyCost ≤ 2(m·n)+n+m+2`.	decoding hardness / SIS one-wayness: imported, not proven. Any “NP-hard” reading conditional on P ≠ NP.
ReLU gate-count `CircuitNet` / `StraightLineCost`	tropical / algorithmic approx.	`compile_eval`: exact (ε = 0) compilation; `compileToDag`: linear gate count `≤ 4N` via sharing-aware DAG; `compile_depth_le`: linear depth; `bellmanStep_compiles_exactly`: exact min-plus / Bellman-Ford gate.	the analytic reciprocal / radical gates remain approximate / imported; depth-vs-width lower bound stays imported (Telgarsky / Eldan-Shamir); model realization not claimed.

The frame, stated plainly. Each instance proves one direction of the find-vs-check asymmetry: an O(·) verifier is machine-checked correct, paired with a soundness theorem that says “if the certificate checks, the answer is right.” The other direction — finding the certificate — stays imported. That is exactly the NP “verification is easy” half, written down seven times across optimization, decision, and number theory.

The tropical / PL core · the resolved DAG linear gate count

Cancellation-free PL circuits compile exactly to ReLU nets at `≤ 4N`.

For arXiv:2606.26705 Thm 3.2 / Cor 5.1's ε = 0 piecewise-linear case, the core machine-checks four interlocking facts. compile_eval: an exact (no ε) compilation of tropical / piecewise-linear circuits to ReLU networks — no approximation. compileToDag: a sharing-aware DAG compilation with a linear gate count ≤ 4N — this closes the previous “linear gate-count claim still needs the DAG / sharing follow-up” caveat that earlier ledger versions carried. compile_depth_le: a linear depth bound. bellmanStep_compiles_exactly: an exact min-plus / Bellman-Ford gate compiling to a ReLU sub-network — the all-pairs DP becomes a tropical network with depth O(k) and gate count O(k³).

Alongside the compilation, three more cores hold the structure together. RegionCount: the linear-region structure is realization-independent — it is an intrinsic invariant of the function, not an artifact of a particular ReLU realization. CancellationFree: the IsMono (cancellation-free) fragment computes exactly the monotone functions; abs_not_isMono makes the contrast precise — abs = max(x,−x) needs the negative scale. DepthSeparation: the tent map's d-fold realizes 2^d linear regions from depth O(d) — cancellation (the negative scale, abs) is essential for that expressivity.

What stays imported. The analytic reciprocal / radical gates (and any non-piecewise-linear primitive) remain approximate / imported; the ε-side of the full Kratsios analytic-gate theorem is not asserted by this core. The depth-vs-width lower bound for general (cancellation-using) neural nets stays imported (Telgarsky / Eldan-Shamir). Learnability is not asserted: the core is about existence of an exact PL compilation, not about whether SGD finds it on data. Model realization (whether a real net realizes the compiled circuit) is not part of the deductive core.

N-1 closed · monotone depth-as-computation

Monotone depth is region-polynomial; cancellation depth is region-exponential.

The slate's gem result, machine-checked across three modules and both axes of the dichotomy. FoldCancellation.isMono_not_iterTent: a cancellation-free circuit cannot realize the d-fold tent for d ≥ 1; folding requires cancellation (isMono_no_fold — a monotone circuit cannot be 1 at 1/2^d and 0 at the larger 2/2^d). isMono_realize1_monotone + isMono_superlevel_isUpperSet: the 1-D realization of any IsMono circuit is monotone with upper-set super-level sets — no oscillation, exactly one rising crossing per level.

On the depth-composition axis: PieceCover.hasPieceCover_iterate — composing a monotone map with itself d times gives ≤ d·k + 1 pieces, linear in depth. The convex-merge linchpin hasPieceCover_max_line shows adding one line to a convex function adds at most one piece (the +1, not +2, is exactly why monotone depth stays polynomial). On the full circuit-structure axis: RegionPoly.isMono_hasPieceCover — every cancellation-free circuit's 1-D realization has a piece count linear in the number of leaves (polynomial in circuit size). N-1 closed on both axes.

What this is and is not. N-1 is a lower bound in the cancellation-free model: it says depth can't help there. It does not bound general (cancellation-using) neural nets, which is the natural-proofs boundary the lane respects. The general depth-vs-width lower bound for ReLU networks (Telgarsky / Eldan-Shamir) is the imported wall this result deliberately leaves untouched.

Honest secondary tier · never headlines

Two more results, honestly tiered.

The lane's discipline: a result's promotion tier matches its receipt. The two below are real findings, but neither is machine-checked end-to-end. They sit beside the headline results, not at them.

N-2 · cancellation spine

One coordinate, honestly bounded.

Retrospective lens: almost every wall the lane hits is the same wall — cancellation. CancellationSpine.isMono_tame machine-checks the load-bearing half on the monotone / convex / region axes (cancellation-free ⇒ tame). The broader reading — that 3SUM (additive), n^ω (subtractive), and analytic gates (division) are all “cancellation-typed” walls — stays an organizing lens, not a reduction theorem: promoting it would need the imported walls themselves formalized, which they are not in any proof assistant.

Tier: [SYNTHESIS]

N-4 · ε-essential region count

Region geometry, modulo trainability.

Empirical: the trained generalization-width threshold tracks ε-essential − 1 at 32 / 36 = 0.89 across families, vs only 18 / 36 = 0.50 for the exact piece count k. Convex families track exactly (1.00). Honest residual: the non-convex jagged family at 0.67 with one outlier (k = 5): SGD failed to find a representable solution the ε-essential count says exists. Generalization onset is region geometry modulo SGD trainability — a clean isolation of the existence-vs-training confound, not a generalization theorem.

Tier: [EMPIRICAL]

Slate-3

Five more — four machine-checked, one empirical.

A fresh hypothesis slate off the same paper, all closed. Each is in the AxiomAudit gate (or, for the empirical one, a deterministic harness with a named falsifier that did not fire).

S3-1 · exact representability

Continuous-PL ↔ finite ReLU net, both ways.

ExactRepr.cpl_iff_reluNet: a 1-D function is the exact realization of a finite ReLU net iff it is continuous piecewise-linear with finitely many pieces. The converse is a peeling induction on the cut set; the forward direction is the non-convex doubling bound. The paper's characterization of universal approximation, at ε = 0, both directions.

Tier: [Lean — axiom-clean, gated]

S3-4 · analytic gate at ε > 0

x² is a ReLU net to any ε — poly and polylog.

The lane's first ε > 0 result. AnalyticGate.sq_eps_approx gives the elementary O(1/√ε)-piece rate (closed-form secant error); SawtoothApprox.sq_polylog_approx gives the polylog O(log 1/ε)-depth rate via the Telgarsky sawtooth — the depth-separation tent put to constructive use, with a one-line self-similar error recursion. Shown for x² — the seed gate that the general construction below iterates to universal approximation.

Tier: [Lean — axiom-clean, gated]

S3-3 · find/check, proved

The ledger's first non-imported gap.

QueryGap.check_lt_find: in a decision-tree (query) model, verifying a supplied witness costs 1 query while any correct existence-decider costs ≥ n (adversary). Both sides machine-checked — the ledger's first proved check ≪ find, where every other instance imports its find-hardness. Honest scope: an unconditional lower bound in a restricted query model, not a P-vs-NP claim.

Tier: [Lean — axiom-clean, gated]

S3-2 · graded cancellation

The dichotomy becomes a dial.

GradedCancellation.hasPieceCover_graded: region count ≤ 4^g · leafCount, where g counts the max gates exposed to cancellation. At g = 0 it recovers N-1's linear bound; each cancellation-exposed fold pays a bounded factor. Cancellation is a graded resource, and the budget bounds the geometry.

Tier: [Lean — axiom-clean, gated]

S3-5 · ε-essential, data axis

Region geometry governs the data, too.

Empirical: at fixed (generous) width, the training-set size needed to generalize tracks the ε-essential region count (Spearman 0.68 noiseless / 0.78 under label noise), while the exact piece count k is flat (≈ 0). With N-4 (capacity axis), the ε-essential count is the learnable invariant on both axes; exact k on neither.

Tier: [Empirical]

The general analytic gate — the constructive ladder, completed

From `x²` to every continuous function, machine-checked.

S3-4 approximated x². Four further modules iterate that one gate all the way to universal approximation — the constructive arc of arXiv:2606.26705's Cor 5.1, each rung axiom-clean and in the gate:

multiply · the hinge

An ε-multiply gate at log depth.

MultiplyGate.mult_polylog: by polarization x·y = ((x+y)² − x² − y²)/2, three rescaled copies of the x² net give an ε-approximate multiply gate of depth O(log 1/ε). Multiplication is the hinge from one gate to all of them.

Tier: [Lean — axiom-clean, gated]

monomial · x^d

Powers by a clamped multiply-chain.

MonomialEval.pow_poly_rate: chaining d−1 multiply gates gives x^d to any ε at depth O(d·log 1/ε). Each step clamps the running value to [0,1] — a contraction, so error never grows and the gate's domain stays valid — and the d errors accumulate only linearly.

Tier: [Lean — axiom-clean, gated]

polynomial · Σ a_ixⁱ

Any polynomial, in the monomial basis.

PolyEval.poly_polylog: an arbitrary polynomial to ε at depth O(deg·log 1/ε). Horner-as-a-circuit is blocked (the running value leaves [0,1]); instead the value stays Horner but the circuit is the monomial sum Σ a_i·(xⁱ net) — only the xⁱ are nonlinear, the linear combination is exact.

Tier: [Lean — axiom-clean, gated]

capstone · universal approximation

Every continuous `f` on `[0,1]` is a ReLU net.

UniversalApprox.continuous_relu_approximable: every f ∈ C([0,1]) is uniformly ε-approximated by an explicit ReLU net. The new machine-checked content is polyEval_approx (every polynomial → net, via a bridge from a mathlib Polynomial to the coefficient list); the single imported analytic input is Stone–Weierstrass (polynomials dense in C([0,1])). Notably the whole theorem stays axiom-clean — Weierstrass adds no sorry and no native_decide.

Tier: [Lean — axiom-clean, gated]

Honest scope: this is the constructive direction of a classical fact. It makes the Yarotsky-style ReLU construction explicit and machine-checked, with density itself cited from mathlib's Stone–Weierstrass. It is not a new approximation-theoretic result, not a rate improvement, and says nothing about learnability or P-vs-NP.

Falsification surface

Named falsifiers — what would void each piece.

Each result declares the witness whose existence would end it. Three already fired their predicted outcome and stayed standing; one (N-2's WALL_WITHOUT_CANCELLATION) is open with status not fired; N-4's EPSILON_REGIONS_ALSO_FAIL did not fire.

Per-result falsifiers

The find/check ledger (N-3): VERIFIER_NOT_PL — a natural certifying problem whose verifier is not straight-line / PL-expressible in the ledger; the certificate exists but the cost model cannot carry it. Status: not fired.
Tropical / PL core: EPSILON_NOT_ZERO_FOR_PL — a piecewise-linear circuit whose compilation requires ε > 0 to a ReLU net. Status: not fired; compile_eval proves ε = 0 across the PL fragment.
DAG linear gate count: SHARING_DOES_NOT_LINEARIZE — a tropical circuit whose sharing-aware DAG compilation is not bounded by 4N. Status: not fired; compileToDag proves the bound.
N-1 (monotone depth region-polynomial): MONOTONE_FOLDS — a cancellation-free (IsMono) circuit whose 1-D linear-region count is super-polynomial in depth. A single such witness ends it. Status: not fired; isMono_hasPieceCover closes both axes.
N-2 (cancellation spine, synthesis): WALL_WITHOUT_CANCELLATION — an imported wall the lane genuinely relies on that is provably not cancellation-reducible. Status: not fired; absence is not a proof, and the additive / subtractive / division axes remain an organizing reading rather than a reduction.
N-4 (ε-essential region count, empirical): EPSILON_REGIONS_ALSO_FAIL — the ε-essential count tracks the trained-generalization threshold no better than exact k. Status: not fired (0.89 vs 0.50 across families, 1.00 within convex families).

Receipts

Public, reproducible, axiom-clean.

Every theorem cited above is in the public sundogcert Lean repo and re-certifies under lake build in seconds. #print axioms shows only [propext, Classical.choice, Quot.sound] for the gated cores (and the lighter axiom set [propext, Quot.sound] for the decidable ones like 2-SAT) — no sorry, no native_decide, no trusted compiler step. The AxiomAudit.lean module pins each headline to Lean's three foundational axioms; a stray axiom fails the build. Lean v4.30.0, mathlib v4.30.0.

Lean modules (`Sundogcert/` in the public repo)

CircuitNet.lean — exact PL compilation + Bellman-Ford
RegionCount.lean — linear-region realization-independence
CancellationFree.lean — IsMono ↔ monotone
DepthSeparation.lean — tent's 2^d
StraightLineCost.lean — the cost measure
FoldCancellation.lean — N-1 sharp negative half
PieceCover.lean — N-1 composition axis
RegionPoly.lean — N-1 circuit-structure axis
CancellationSpine.lean — N-2 isMono_tame
ExactRepr.lean — S3-1 cpl_iff_reluNet (continuous-PL ↔ ReLU)
GradedCancellation.lean — S3-2 hasPieceCover_graded
AnalyticGate.lean — S3-4 sq_eps_approx (x² at ε > 0, poly)
SawtoothApprox.lean — S3-4 sq_polylog_approx (polylog depth)
MultiplyGate.lean — mult_polylog (ε-multiply, the hinge)
MonomialEval.lean — pow_poly_rate (x^d, clamped chain)
PolyEval.lean — poly_polylog (any polynomial, monomial basis)
UniversalApprox.lean — continuous_relu_approximable (capstone, + Weierstrass)
Certifies.lean — LP-duality core, weakDuality_tight
MaxFlowMinCut.lean — maxflow_mincut
MatchingCover.lean — konig
TwoSat.lean — check_correct + cert_sound
PrattCert.lean — prime_iff_witness
ShortestPathCert.lean — cert_isLeast
QueryGap.lean — S3-3 check_lt_find (proved find/check gap)
AxiomAudit.lean — the gate

Narrative receipts (`docs/`; shipped publicly via `dist/`)

ALGO_APPROX_CONJECTURE_SLATE_2.md — slate with status
ALGO_APPROX_CONJECTURE_SLATE_3.md — slate-3, all five closed
ALGO_APPROX_N2_CANCELLATION_SPINE.md — synthesis lens
ALGO_APPROX_N4_EPS_REGIONS_RESULT.md — empirical (capacity axis)
ALGO_APPROX_S35_SAMPLE_COMPLEXITY_RESULT.md — S3-5 empirical (data axis)
ALGO_APPROX_CD2_GROKKING_RESULT.md — the prior null this redeems
SUNDOG_V_CERTIFICATE_LEAN.md — the parent ten-example ledger
SUNDOG_V_ALGO_APPROX.md — the lane ledger
github.com/humiliati/sundogcert — the Lean repo
arXiv:2606.26705 — Kratsios et al.

Sibling lanes

/p-vs-np — bounded alignment-verification, the find/check sibling
/generality — high-stakes generality umbrella
/navierstokes — the NSE C1 Reading-2 witness lane (review-gated)

Cheaper to check than to find. Machine-checked across seven problems.

Seven CHECK-side theorems under one interface.

Cancellation-free PL circuits compile exactly to ReLU nets at ≤ 4N.

Monotone depth is region-polynomial; cancellation depth is region-exponential.

Two more results, honestly tiered.

One coordinate, honestly bounded.

Region geometry, modulo trainability.

Five more — four machine-checked, one empirical.

Continuous-PL ↔ finite ReLU net, both ways.

x² is a ReLU net to any ε — poly and polylog.

The ledger's first non-imported gap.

The dichotomy becomes a dial.

Region geometry governs the data, too.

From x² to every continuous function, machine-checked.

An ε-multiply gate at log depth.

Powers by a clamped multiply-chain.

Any polynomial, in the monomial basis.

Every continuous f on [0,1] is a ReLU net.

Named falsifiers — what would void each piece.

Per-result falsifiers

Public, reproducible, axiom-clean.

Lean modules (Sundogcert/ in the public repo)

Narrative receipts (docs/; shipped publicly via dist/)

Sibling lanes

Cancellation-free PL circuits compile exactly to ReLU nets at `≤ 4N`.

From `x²` to every continuous function, machine-checked.

Every continuous `f` on `[0,1]` is a ReLU net.

Lean modules (`Sundogcert/` in the public repo)

Narrative receipts (`docs/`; shipped publicly via `dist/`)