# Proofs, executable policies, and numerical certificates Fovea uses **gdp-wired 0.30.1**, an exact-pinned development dependency. There is no Bend compiler dependency. Bend-language extraction remains supported. An optional independent development checks stronger abstract numerical models with Lean 4.19.0 and pinned mathlib. Neither development, packaging nor the required CI gate needs Lean. Neither model development proves that the complete Float64/CSR implementation refines its mathematical model. ```sh bun run check:proofs # all required laws checked, then byte-for-byte generation bun run proofs:generate # deliberate regeneration after proofs pass bun run proofs:artifact # source/bridge/output receipts, without loading the prover bun run check:streams # 98 arithmetic stream claims; no Lean needed bun run check:series # 23 constructive-series claims; no Lean needed bun run check:completion # 19 rational completion certificates; no Lean needed bun run check:residual # finite binomial coefficient/evaluation claims bun run check:operator-identity # 114 composed finite-rational operator claims bun run check:operators # 24 coefficient/path claims; no Lean needed bun run check:transport # 14 indexed-transport claims; no Lean needed bun run check:focus # 19 indexed focus/row-gather claims; no Lean needed bun run check:enclosures # 7 exact quotient/interval claims; no Lean needed bun run check:normalization # 17 raw-row and rescaling claims; no Lean needed bun run check:ports # scoped inventory of all 28 retained Lean claims bun run check:lean:artifact # model receipt freshness; no Lean loaded bun run check:lean # full Lean check; requires FOVEA_MATHLIB_ROOT bun run check:fast # gdp proofs, generated receipts, types, affected tests ``` ## Authored sources and generated artifacts The definitions in `proofs/*.ts`, adapters in `proofs/runtime/*.ts`, and proof-checking scripts are included in strict TypeScript checking. `proofs/types.ts` describes the mutually exclusive invariant, consequence, transition, fold, and loop proof modes; the checker still validates modes and support provenance at runtime. TypeScript checks implementation contracts; gdp-wired independently checks the mathematical claims. Neither check substitutes for the other. Development commands execute TypeScript through `tsx`. The source auditor parses TypeScript before importing the prover, follows local type imports for receipt hashing, and rejects dynamic/import-equals imports, effectful dependencies, and unproved foreign facts. Artifact-only checking does not load gdp-wired. It still uses the development toolchain; installed extension/CLI execution does not. `bun run format` and `bun run format:check` use pinned Prettier for authored code. Generated JavaScript is emitted without minification and formatted by the generator. Control, limb, and stream declarations are derived from typed adapters; the kernel ABI remains independently declared in `proofs/kernel-abi.json`. Formatter versions are bound into the artifact receipt. Never hand-edit generated files. Test fixture sources are excluded from formatting because their text and positions are test data. ## What executes `proofs/kernel.ts`, `proofs/controls.ts`, and `proofs/limbs.ts` define symbolic functions. Independent specifications are in `proofs/laws.ts` and `limbLaws` in `proofs/limbs.ts`. The exact functions being proved are passed to gdp-wired's `compileJs`; no handwritten alternate implementation supplies the policy result. Every proof must be both `proven` and `checked`. The gate rejects unexpected assumptions and checks the complete required law inventory against `proofs/ledger.json`. The generator emits four standalone modules: - `src/verified/generated/kernel.js`: disclosure, prefix accounting, basis commands. - `src/verified/generated/control.js`: semaphore admission/handoff, capacity, lease validity, focus invalidation, prefix selection. - `src/verified/generated/limbs.js`: audited arithmetic cells and executed rounding/work decisions. - `src/verified/generated/streams.js`: executed comparison, addition, subtraction, multiply-add rows and short-division certificates. The adjacent declarations retain the four kernel export names. Their numeric ABI is now **number-valued u32 (0..2^32-1)**, not BigInt; out-of-range inputs and outputs throw rather than wrapping. `VERIFIED_NAT_MAX` is `0xffffffff`. `BEND_NAT_MAX` is a deprecated name for that new limit, not the old 48-bit limit. This deliberately changes direct internal-kernel callers; normal renderer and heat APIs already use numbers. Abstract policy laws still quantify over mathematical naturals; checked codecs restrict executed values to u32. The manifest binds proof sources, required-law inventory, ABI, codecs, scalar numerical source, generator, toolchain versions and generated bytes with SHA-256. Checking never rewrites; explicit generation writes only after proofs and code generation succeed. CLI packaging verifies these same source/output receipts. Neither the installed extension nor the bundled CLI needs gdp-wired or a compiler. ## Coverage ledger: 405 checked claims | Family | Laws | Production connection | | --------------------------------- | ---: | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | Disclosure | 6 | Executed generated decisions in both focus/dwell rendering paths. | | Prefix accounting | 5 | Executed shown/remaining counts in both renderers. | | Basis commands | 4 | Executed commands control Chebyshev vector extension. | | Semaphore | 7 | Executed acquisition/release decisions, including reserved handoffs. | | Capacity | 3 | Executed root admission and shared cache trimming. | | Leases | 4 | Executed epoch/lease/presence checks before late results are accepted. | | Focus lifecycle | 4 | Executed fresh/key/generation reset decisions and stale dwell rejection. | | Prefix selection | 4 | Executed admission for every actual rendered-prefix cost. | | u32 arithmetic cells | 11 | Retained generated primitive contracts; production multiword operations now use the stronger streams below. | | Arithmetic streams | 98 | Executed digit machines, all-prefix reconstruction, completion, intermediate bounds, termination and checked ghost erasure. | | Rounding decisions | 7 | Executed floor, directed ceiling and nearest-even choices in limb shifts and Float64 conversion. | | Certificate work | 3 | Executed admission of normalization and operator visits; refusal leaves the budget unchanged. | | Sparse edge execution | 7 | Generated cursor admission, progress, coordinate bounds, refusal and gather/scatter direction. | | Exact heat algebra | 4 | Mathematical fold model; not the Float64 matrix implementation. | | Signed error envelope | 1 | Conditional rational model; local numerical bounds are premises. | | Constructive series | 23 | Exact rational Cauchy model: finite-tail bounds, nested enclosures, explicit modulus, arbitrary future prefixes and scalar-family identities. | | Constructive completion | 19 | Shrinking rational enclosures, all-future checkpoint bounds, finite product/reciprocal continuity and rational separation witnesses. Not yet an operator-limit identification. | | Finite-rational operator identity | 114 | Coefficients, indexed evaluation, finite reindexing, all-later-prefix bounds, terminating precision selection and constructive Cauchy-name comparison. | | Coefficient and path models | 24 | Unbounded Pascal/factorial coefficients, signed P-I recurrence, normalized weighted-tree mass and signed-aggregate bounds. Not the indexed matrix evaluator. | | Indexed transport | 14 | Actual finite-map L1 norm, source-weight budgets and arbitrary completed normalized transport rounds. Exact model, not a proof of the CSR/interval implementation. | | Indexed focus | 19 | Coordinate-wise infinity-norm bound through arbitrary completed row-gather rounds, exact weight consumption and row coverage. Not a CSR/IEEE refinement. | | Exact enclosures | 7 | Natural quotient bounds and scaled-rational interval/error policies; not real completion or host rounding correspondence. | | Raw-row normalization | 17 | Native finite-map unit mass, exact raw ratios, rescaling, isolate identity and consumer admission. Production uses an exact dyadic adapter; the host refinement is still unproved. | **152 claims are connected to executed policies, streams or sparse edge steps; 11 older arithmetic cell contracts, five heat/error laws, 23 constructive-series claims and 24 coefficient/path claims, 14 indexed-transport claims, 19 indexed-focus claims and seven exact-enclosure claims, 17 raw-row normalization claims and 19 constructive-completion claims are retained as separate mathematical contracts.** Stream counts include named termination checks as well as invariants and corollaries, not just one-step decisions. This does not prove all callers, filesystem effects, callback ordering, matrix dimensions or source-to-JavaScript translation. Boundary and integration tests remain. ### Executed arithmetic streams, not a separate twin `proofs/streams.ts` defines the machines that `compileJs` emits for production. The proof adds unbounded **ghost** accumulators for input/output values and positional powers. These are mathematical state only: no wide integer is stored in a JS number, and no runtime BigInt is introduced. A product-machine proof checks that every observable runtime state agrees before and after removing the ghosts. Termination ranks use the same transitions as the generated code. The five machines establish: - Comparison agrees with the exact values of every consumed most-significant-first prefix. - Addition and subtraction reconstruct every little-endian prefix, including final carry, exact underflow and the retained nonzero extent. - Multiply-add rows accept low/high digits only when their equation reconstructs the exact product plus accumulator and carry. The complete row is proved, including its final carry; a corrupt digit is refused. - Short division accepts quotient/remainder digits only when they reconstruct the current numerator and leave a smaller remainder. Every accepted prefix satisfies the complete quotient/remainder relation; invalid witnesses stop. - All executed scalar state is u32-sized. Integer intermediates are explicitly bounded to at most 33 bits for add/subtract, 32 bits for a multiply-add cell and 48 bits for short division; those integers are exact in JavaScript. `check:streams` automatically builds proof trees and checks them independently. Stronger equality-product search is scoped and restored. Derived claims may use only a previously checked invariant group and already checked consequences of that same group; input-safety claims additionally use the enforced input kinds. It accepts no new foreign facts. The checker has per-goal and whole-check deadlines. Runtime adapters explicitly validate parameter bounds rather than assuming the generator enforces them. This is **not yet a fully verified multiword library**. Array capture, packing, output materialization, the outer schoolbook multiplication traversal, general long division and shifts remain host obligations. The stream theorems quantify over arbitrary finite prefixes, not merely the lengths exercised by tests. ### Constructive series: a checked route through finite arithmetic `proofs/series.ts` does not introduce an `exp` axiom or assume convergence. It represents rational approximations with unbounded natural numerators and denominators. With `d = n + gap`, `gap > 0`, its actual transition is: ```text v = d + growth (growth is any natural) D' = D v; T' = T n; S' = (S + T) v L = S / D; U = (gap S + d T) / (gap D) ``` Starting at `D=1, T=C, S=0`, the checker proves: - Positive denominators and the finite-tail bound `gap S + d T <= d C D`. - Lower endpoints never decrease; upper endpoints never increase. - A Bernoulli majorant `(d + k gap) T <= d C D`. - For every positive precision integer `q`, the explicit modulus `K(q) = q d² C` implies `U - L <= 1/q` at every `k >= K(q)`. - A checkpoint can capture **any** prefix. If its index is at least `K(q)`, **every later prefix**, regardless of future nonnegative growth inputs, differs from the saved lower endpoint by at most `1/q`. The last claim is a universal Cauchy estimate, not testing a finite set of prefixes or merely assuming the existence of a limit. Conservative nonnegative slack variables expose exact conservation equations; all those equations are also checked. The modulus is an existence witness, deliberately not a proposed runtime iteration count. The model is proof-only: its huge exact values are not executed as JS numbers or added as runtime BigInts. Six further claims prove that exponential/Poisson and Bessel denominator recurrences instantiate this model, and that a valid finite tail cutoff exists for **every nonnegative rational argument**, not only the supported `[0,64]` runtime domain. An initial rational `C/B` uses these enclosures divided by `B`; for positive natural `B`, the same modulus is conservative. Production scalar series and the vector verifier now share `interval.ts`'s `geometricTail`: at the first tail term, `n=ratio`, `d=SCALE`, `gap=SCALE-ratio`, and `C=next` give exactly its rational bound before outward rounding. `scripts/prove-polynomial.ts` is **untrusted search**, not a new kernel. It constructs exhaustive natural-factor cuts and bounded products of existing inequalities, then uses gdp-wired's solver to construct proof trees. Every tree is replayed by the existing `gdp-wired/kernel.check`; there are no foreign facts, new axioms or kernel modifications. The shared checker validates support lists, proves every initial and inductive case, and allows derived premises only after they have been checked in the same state context. Cyclic and input-dependent premise escapes are refused. Search is capped by time, tree visits and products. ### Constructive completion certificates `proofs/completion.ts` starts the replacement's limit layer with **19 checked claims**, using the existing gdp-wired kernel and no foreign mathematical facts. Its refinement machine builds nested intervals `[lower / scale, (lower + width) / scale]`, doubles `scale` at every step and retains arbitrary checkpoints. The checked linear modulus `index >= p * width` implies interval width at most `1/p` for positive `p`. Checkpoint bounds apply to all subsequent reachable states, with no maximum precision or iteration count. Separate finite certificates establish the exact kept-rectangle/tail partition of a product, its bounded-factor continuity estimate, positive reciprocal width, and two-sided error composition. A positive rational gap `g/d` is separated at precision `d+1`; testing only finitely many earlier precisions does not establish equality. Tests retain that deliberately false variant, missing product terms, nonshrinking denominators and invalid refinements, with independent BigInt oracles. These are supporting **finite certificates for constructive completion**. They are not by themselves the operator identity: that argument also needs the producer/consumer links, finite reindexing and all-later-prefix estimates below. Rational-gap separation is not a decision procedure for equality of arbitrary real limits. The public `check:completion` command and the composed `check:operator-identity` command are part of `check:proofs`; their sources and checkers are receipt-bound. The broader 28-claim Lean development is retained as an optional independent audit, not silently relabeled as equivalent. ### Finite binomial cancellation `proofs/residual.ts` constructs the fixed Pascal row and the actual signed coefficients of every `(P-I)^j`, then accumulates them with `choose(m,j)`. Its coefficient laws prove, for arbitrary natural `m` and every coefficient `k`, ``` sum(j=0..m, choose(m,j) * coefficient(k, (P-I)^j)) = (k == m ? 1 : 0). ``` The telescoping invariant and boundary coefficients are checked rather than supplied as assumptions. The proof reuses 19 checked Pascal claims. Positive-factor cancellation needed bounded products of linear inequalities in the **untrusted search**, not a new axiom: the unchanged gdp-wired kernel validates each product certificate. The option is disabled for other proof groups. ### Composed finite-rational operator identity `check:operator-identity` checks 114 distinct operator claims, including the coefficient laws above. Prerequisite Pascal and indexed-focus claims retain their original ledger entries. For a finite rational row-stochastic `P`, with the induced infinity norm, and nonnegative rational `t=a/b` (`b>0`), define ``` E_N = sum(j=0..N, t^j/j!) S_N = sum(j=0..N, t^j/j! P^j) A_N = sum(j=0..N, t^j/j! (P-I)^j). ``` The checked components are: - `cauchy-product.ts`: finite signed sums preserve their exact total when rectangular product terms are grouped by `i+j`; diagonal bounds and their inverse match the truncated rectangle. Power multiplication and factorial coefficient scaling are checked separately, without assumed `exp` functions. - `residual.ts`: the actual signed coefficient producer, its bounded evaluation, and exact low-degree cancellation. `operator-identification.ts` checks the actual series-admission guard on its output, and the actual indexed stochastic gather's output against the evaluator's basis guard. A caller's assertion that two independently chosen models agree is not accepted. - `residual-series.ts` and `residual-link.ts`: exact assembly, positive `E_N`, and a refinement into the Taylor-tail recurrence with arbitrary row denominators. This yields the finite residual estimate `||E_N A_N-S_N|| <= sum(m=N+1..2N, (3t)^m/m!)`, and both unnormalized and normalized precision bounds for **every later prefix**, not a fixed sample. - `operator-limit.ts`: a terminating computation of `C=(3a)^d`, `d=6a+1`, bound to the actual Taylor recurrence's initial majorant. The explicit cutoff `K(q)=d+q*d*d*C` works for every positive natural precision `q`. The checked three-error inequality transfers the Cauchy property and equality of the two names; rational separation rules out a positive gap. Consequently the constructive Cauchy names `A_N` and `S_N/E_N` represent the same limit. Here the operator exponential is **defined by the Taylor name**; this is the finite-rational Poisson identity, not a claim of equivalence to Lean's theorem over every complete normed real algebra. Completion uses the usual identification of Cauchy names whose difference tends to zero; no finite-prefix agreement is substituted for that universal condition. The rational matrix tests are independent examples, not the proof. Quantified invariant reuse is instantiated through the kernel's native `assumed` operation; tests reject a different key, an omitted instantiation, cyclic dependencies, changed grouped sums, and a nonterminating precision plan. No gdp-wired kernel or mathematical axiom was changed. The Float64/CSR refinement, numerical codec and full fast-solver error theorem remain separate obligations. ### Finite Poisson coefficients and normalized paths `proofs/operators.ts` constructs complete Pascal rows, factorial witnesses and parity bits over unbounded natural numbers. Its 19 invariants include, for every reachable row `n` and every `0 <= k <= n`: ``` B[k] * K[k] * R[k] = n! K[0] = 1, K[k] = k * K[k-1] R[n] = 1, R[k-1] = (n+1-k) * R[k] K[k] > 0, R[k] > 0 ``` These are quantified statements, not proofs up to a selected degree. The index and factorial witnesses are built inside the transition; no foreign factorial or binomial facts are assumed. The model stays proof-only: its unbounded values are not executed using JS Number in production. `proofs/operator-steps.ts` adds two checked one-step laws. With the constructed parity `Q[j]`, define `C_n[k] = (-1)^Q[n-k] B[k]`, zero outside the row. The positive/negative pair satisfies exactly the coefficient shift-and-negate recurrence for multiplication by `P-I`. Together with the factorial invariant, this supplies the finite coefficient algebra behind ``` C_n[k] / n! = (-1)^(n-k) / (k! * (n-k)!) ``` The same file proves three structural-induction laws for every finite normalized binary weighted tree, with no depth bound. Every leaf has signed parts summing to the input mass `M`; every internal pair of nonnegative weights sums to its positive divisor. The exact common denominator stays positive, the positive and negative numerator sum is `M * denominator`, and their absolute difference is no larger. Arbitrary-depth weighted composition is covered **in this path model**. This is a signed-aggregate bound, not yet the L1 norm theorem for an indexed matrix: grouping leaves by output coordinate and correspondence to the actual sparse traversal remain separate obligations. The search uses one bounded round of intermediate monomials to substitute factorial witnesses through products. Kernel rules have not changed. The shared checker admits quantified instances only from checked invariant groups and checks native one-step and fold obligations; it never reuses a step law as an invariant. Tests include exact BigInt oracles through degree 32, a deeper weighted tree, corrupt certificates, broken coefficients/parity, and missing normalization. ### Indexed signed transport and arbitrary rounds `proofs/transport.ts` closes the gap between a single signed aggregate and a finite indexed vector **in the exact model**. Two sparse buffers alternate as source and destination. A coordinate is stored canonically as `(p,n)` with `p=0` or `n=0`; opposite signs cancel at each destination update. Consequently, `sum(p+n)` is the vector's actual L1 norm, not an uncancelled mass envelope. The sums are native gdp-wired finite-map sums, over all keys with no size bound. Each source is removed into a pending column, receives a positive integer weight budget `D`, and emits nonnegative integer weights until that budget is exhausted. A round can flip buffers only when no nonzero source remains and the pending budget is zero. The common rational denominator then multiplies by `D`. Arbitrary rational column-stochastic weights can use a common denominator; isolates emit all `D` units to themselves. There is no fixed graph, dimension or round limit. The checked invariants include canonical coordinates, positive denominators, weight bounds, and ``` bound = initialNorm * denominator D * sourceL1 + remaining * pendingL1 + destinationL1 <= D * bound ``` They imply `sourceL1 / denominator <= initialNorm` after every state, including every completed round. Separate native step laws check completed output bounds, round/denominator progress, and exact weight consumption. Seed inputs are a magnitude and sign, so `initialNorm` is the actual input norm. Tests independently execute the expressions with BigInt, recompute map sums, and compare eight sparse matrix powers with cancellation and an isolated high-index coordinate. This does **not** remove the production boundary: the encoder from CSR traversal to this protocol, interval rounding, and the analytic exponential identity still need correspondence proofs. The installed runtime has not been changed to this proof-only transport model. The complementary focus/infinity-norm protocol is checked below; neither model is yet a refinement proof of the production traversal. ### Ported focus and interval policies `proofs/focus.ts` gives the transpose companion: row-stochastic gathers over two sparse buffers with canonical signed coordinates. Seed inputs must fit a supplied natural bound `M`; any rational vector can choose its actual infinity norm after common scaling. The source buffer is immutable while rows are gathered. Each row consumes exactly `D` weight units before committing, and a cursor must visit all `size` rows before buffer rollover. Empty vectors, zero weights, repeated neighbors and isolated identity rows are allowed. There is no dimension or round cap. The kernel checks both buffers' coordinate bounds, the accumulator budget `pendingP + pendingN + remaining*bound <= D*bound`, and `bound = M*denominator`. These give the true infinity-norm bound at every completed round. A separate step law prevents claiming completion with skipped rows. BigInt tests compare repeated sparse matrix powers, test source-buffer immutability, and require rejection of removed weight/coverage guards. `proofs/enclosures.ts` ports seven interval policies to natural arithmetic: quotient floor/ceiling bounds, addition, nonnegative multiplication, positive-denominator division, signed subtraction and the certificate endpoint error implication. Cross multiplication represents rational comparisons; common positive scaling and, for affine signed comparisons, a common offset avoid lossy floating-point arithmetic. Quotient policies require a checked Euclidean witness `n=q*d+r`, `0<=r=0} (t^k / k!) P^k a. ``` Weights are decoded as exact dyadics, lifted to common integer units and summed exactly before probability division is rounded outward. This avoids overflow, all-subnormal denominators and pre-normalization fixed-point rounding. Signed vectors are split into positive and negative parts. Every finite operator application and sum propagates outward intervals. Row-stochastic focus is nonexpansive in the infinity norm; column-stochastic forward transport is nonexpansive in the one-norm. If the last included term has index k and `t/(k+2)<1`, the omitted coefficient mass is bounded by ``` (exp(-t) * t^(k+1)/(k+1)!) / (1 - t/(k+2)). ``` The implementation evaluates an upper enclosure of this bound, multiplies it by an upper bound on the appropriate source norm, and enlarges both ends of each signed output interval. It returns `maxAbsoluteError`, an outward-rounded upper bound on the distance from the actual candidate to that enclosure. `withinTolerance` is true only when that upper bound fits the requested absolute tolerance. A corrupt candidate or corrupt degree vector is not silently certified. **This closes a runtime verification gap, not every formal-proof gap.** The returned `assumptions` records dependence on the limb/interval implementation, JS semantics, the exponential/Poisson series identity, and stochastic norm bounds. The analytic identity, limiting geometric-series argument and norm bounds now have checked Lean model theorems. Their instantiation by the actual limb/vector evaluator is still unproved, so the runtime assumptions are retained. Seven laws cover the actual rounding decisions; three cover actual work admission. Neither set is a proof of the complete evaluator. The evaluator allows at most 512 Poisson iterations and a configurable reference work cap of at most 1,000,000 normalization/operator visits (default 100,000). This counts structural visits, not seconds or limb instructions; running the fast candidate is additional work. Invalid CSR/data, insufficient fixed-point precision, exhausted work, or nonfinite output bounds fail closed. A valid candidate that exceeds tolerance returns `withinTolerance: false`. ## Remaining numerical theorem An unconditional, machine-checked matrix-exponential theorem is still open. The fast solver itself would require proofs composing: 1. CSR/degree normalization error and the operator's norm bound; 2. scalar coefficient intervals and the omitted Chebyshev-series tail; 3. recurrence and vector-summation roundoff; 4. any coefficient pruning and the similarity transforms around the solver. The separate Lean development supplies analytic ingredients for the Poisson reference, not this Chebyshev proof or a refinement proof of either TypeScript implementation. A passing rational bookkeeping theorem does not discharge it. The independent scaled-Taylor tests, conservation tests, recurrence parity tests and threshold counterexample remain. In particular, increasing diffusion time does not universally increase a thresholded lit set. ## Trust and regression gates Trusted for executed policies: gdp-wired's checking kernel, the generator/ABI bridge, numeric codecs, JS engine and host effect interpreters. The numerical certificate implementation is still trusted. For the separate model theorems, the Lean kernel, pinned mathlib environment and its standard axioms are trusted; Lean is not loaded by the installed product. The untrusted prover's result alone is never accepted. A source receipt is freshness evidence, not a cryptographic proof certificate. The proof-source import checks are a development safety guard, not a sandbox for hostile JS. `tests/series.test.ts` executes the constructive model with independent BigInt arithmetic, checks large rational-family instances, refuses circular or input-dependent proof premises and verifies that corrupted polynomial proof trees are rejected. This is separate from the universal proof gate. `tests/streams.test.ts` checks actual production dispatch, long carry/borrow chains, whole-row equations, invalid digit witnesses, runtime bounds and ghost erasure. `tests/proofs.test.ts` also mutates a stream, its reconstruction invariant and its projection, requiring the autoprover to refuse each change. `tests/lean-proofs.test.ts` rejects stale model sources, missing theorems, altered axiom audits, proof escapes and claimed TypeScript correspondence. With `FOVEA_MATHLIB_ROOT` set, it also gives Lean a false unbounded addition theorem and requires failure before the receipt can be overwritten. The manually triggered Lean CI job runs that independent audit; normal push/PR checks use gdp-wired and do not depend on the Lean receipt. `tests/proofs.test.ts` mutates policies, imports, ABI and artifacts and requires refusal without writes. `tests/verified-kernels.test.ts` checks ABI boundaries and spies on actual renderer/heat consumers. `tests/asyncutil.test.ts` tests the real handoff schedule, and `tests/numerics.test.ts` exercises scalar certificates. `tests/heat-certificate.test.ts` checks analytic solutions, signed fields, isolates, extreme weights, corrupt candidates/degrees, and bounded refusal. `tests/interval.test.ts` independently checks interval endpoints with BigInt. `tests/u32.test.ts` compares multiword loops, shifts, quotient/remainder, and Float64 rounding with an independent BigInt oracle (BigInt is test-only here). Direct lease/reset/capacity truth-table examples and duplicate count examples were removed: their laws are checked on every proof gate. ABI boundaries, overflow refusal, real eviction and semaphore interleavings remain tested. Startup tests require registration to remain analysis-free and under its existing byte budget. No budget was raised and no numerical suite was retired.