Scanpy has a proved output checker with a trusted execution bridge. DESeq2 has translated-model invariants with finite output comparisons. Neither has an implementation-refinement proof.
In the real-valued translation, positive sample scaling preserves the retained rows and normalized between-sample ratios. Size factors follow a proved scaling identity.
Boundary
A chosen 10^-12 tolerance checks recorded-output consistency. It does not prove accuracy against the ideal estimator or R/libm refinement.
The exact-real estimator is exp(median(log ratios)); even medians average central log values. For positive scales c and nonempty all-positive retained rows, s(K scaled by c)[j] = (c[j] / G(c)) * s(K)[j], where G(c) = exp(mean(log(c))).
Assumptions
The mathematical model has finite real-valued count rows, positive sample scales and at least one row positive in every sample.
The target uses the default ratio method and stats::median; even medians average the central log values.
The production interpretation uses dense nonnegative counts, at least one sample and one all-positive row, without missing or nonfinite values.
R execution, binary-output recording and Python decoding faithfully represent the executed function and observed values.
Outside the claim
A chosen 10^-12 tolerance checks recorded-output consistency. It does not prove accuracy against the ideal estimator or R/libm refinement.
No formal R refinement, universal floating-point accuracy bound, full-package verification or statistical validity claim.
No poscounts, supplied geoMeans, custom location functions, control-gene indexing or other DESeq2 routines.
Execution used the unchanged upstream function assignment with dependencies; the full package namespace/S4 route was not tested or proved.
Proof artifact
Lean 4.32.2 and pinned Mathlib prove invariants of exp(median(log ratios)), including even-row log medians. An independent mathematical review passed 10 scope and theorem checks.
R/libm floating-point correspondence remains unproved. Exact rational certificates compare recorded outputs, not output accuracy against the ideal estimator. The unchanged upstream function assignment ran with dependencies; the full package namespace/S4 route was not exercised.
The unchanged function assignment ran on 10 synthetic matrices. The 59 kernel-checked comparisons satisfy a chosen 10^-12 tolerance, not a proved numerical error bound or accuracy guarantee against the ideal estimator. The largest observed residual is about 3.7e-15.
Lean 4.32.2 kernel, pinned Mathlib and axioms propext, Classical.choice and Quot.sound.
Source/hash checks, unchanged R function execution, R/libm, binary-output recording and Python binary64 decoding.
The connection from the intended algorithm to the real-valued translation; no proof of numerical implementation correspondence.
Review basis
Independent mathematical review reported 10 passed checks at the pinned contribution commit. Reviewed source hashes match this catalog. The full contribution gate was replayed separately in an isolated copy.
Next obligation
Establish accuracy against the ideal estimator and production floating-point correspondence before considering an implementation-refinement claim.
2026-10-02 · revision 2 · corrected. Accepted translated-model invariants and finite production-output comparisons after a copied gate rerun. Kept the main claim at model-only assurance.
2026-10-02 · revision 3 · corrected. Attached the passed independent mathematical review. Retained model-only status and clarified that consistency certificates do not establish ideal-estimator accuracy.
A proved checker accepted outputs from 41 actual Scanpy runs on synthetic count matrices. It checked grouped sums, labels and supplied source witnesses.
Boundary
No Scanpy implementation refinement. Python extraction and adapter-supplied source witnesses remain trusted.
ScanpyAggregate.check_sound proves the stated contract for accepted serialized input/output pairs. This checks observed outputs; it does not refine the original Scanpy implementation.
Assumptions
Python faithfully extracts and serializes the actual input and output, and decodes observed binary64 values with as_integer_ratio.
Source-index/name witnesses are adapter-supplied. Scanpy does not return them; Lean checks them against the serialized input.
The pinned packages, JIT configuration and runtime load correctly. The execution environment remains trusted.
The declared input domain, group ordering, labels and Boolean mask match the actual call.
Outside the claim
No Scanpy implementation refinement. Python extraction and adapter-supplied source witnesses remain trusted.
No Python, Numba, SciPy or AnnData refinement; no IEEE-754 reduction proof.
No other reducers or axes, multiple group columns, negative/general floating inputs, layers, GPU, Dask or backed data.
No whole-package correctness, statistical calibration, biological validity or upstream endorsement.
Proof artifact
A general Lean-proved output checker establishes sum, identity, coverage and bound properties. Fourteen corrupted or unsupported transcripts have kernel-proved rejections. Independent mathematical review passed 10 checks; original Scanpy implementation refinement remains unproved.
Python extraction, serialization and binary64 decoding are trusted. Source-index/name witnesses are adapter-supplied, not returned by Scanpy. Lean checks these witnesses against the serialized input; it does not establish their origin in execution.
41 actual Scanpy executions on synthetic matrices passed the proved checker across dense, CSR and CSC backends. The copied contribution gate reproduced all seven deterministic artifacts.
Adapter-supplied source witnesses and their correspondence with the executed data; the compiler/JIT, runtime and operating system.
Review basis
Independent mathematical review reported 10 passed checks at the pinned contribution commit. Both reviewed proof source hashes match this catalog. Module compilation and replay passed; that review did not rerun Scanpy or rebuild the imported dependency environment. The contribution gate was replayed separately in an isolated copy.
Next obligation
Establish execution correspondence before considering any implementation-refinement claim. Python extraction, serialization, binary64 decoding and adapter-supplied source witnesses remain trusted.
2026-10-02 · revision 2 · corrected. Accepted the completed proved-output-checker contribution after an isolated full gate rerun; status describes runtime output checks, not Scanpy refinement.
2026-10-02 · revision 3 · corrected. Attached the passed independent mathematical review after matching both proof sources. Retained runtime-checked status and explicit trusted adapter/source-witness boundaries.
HolmStat.checked_reporting_fwer bounds the unconditional accepted-and-false-rejection event for the frozen exact Holm formula. It does not bound error conditional on acceptance.
Assumptions
A finite probability law has nonnegative rational weights that sum to one, with represented rational p-values.
The hypothesis family, true-null subset and alpha are fixed across outcomes.
Each true-null p-value meets the stated marginal validity bound. Independence is not required.
Only checker-accepted decisions are reported; failed checks report no rejections.
Outside the claim
This is Veriformatics’ own component. It does not verify R stats::p.adjust, DESeq2 or Scanpy.
No proof of real-data p-value validity, selection practice, biological truth or arbitrary continuous probability laws.
No native compiler, parser, R/Python adapter or deployed execution correspondence is proved here.
Proof artifact
The retained Lean 4.34.1 sources rebuilt locally. All 24 audited declarations use only the listed standard axioms. The build record is unsigned.