# SciGround Math — scoped validation summaries

This is the public summary accompanying /math/. It reports bounded mathematical
and implementation validations; it is not a raw reproduction package or an
end-to-end benchmark of every product workflow. The page describes the
release-integrated product; these measurements keep their original scope.

## Results

### Robust to every exclusion.

18,473 — exclusion cases, every one checked.

In a two-group count model, removing any set of up to three of 48 observations leaves the direction of the estimated effect unchanged—proved for every case and confirmed by a separate checker.

Evidence: [Scaling-certification integration record](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/docs/RESEARCH-INTEGRATION-20261020.md)

### Built for genome scale.

15,285 — hypotheses at genome scale.

Certified discoveries across 15,285 hypotheses in semi-synthetic genome-scale count data. Exact reference laws for every gene compute in 9 seconds for a 12 + 12 design.

Evidence: [Genome-scale implementation results](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/foundation-20261002/workflow-a5d/impl/RESULTS.md)

### More discoveries. Same guarantee.

+55% — true discoveries at the same error bound.

Protected scoring raised average true discoveries from 4.08 to 6.34 across 99 held-out conditions, and the chance of at least one true discovery rose too—with the false discovery rate within the declared bound (common-U e-BH).

Evidence: [Practical-usefulness synthesis](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/foundation-20261002/practical-usefulness-synthesis-20261021/SYNTHESIS-REPORT.md)

### Real DESeq2, rigorously bounded.

162,323 — DESeq2 values rigorously enclosed.

Normalisation and initial dispersion values from actual DESeq2 1.42.0 runs on public RNA-seq data, enclosed in rigorous bounds across five analyses.

Evidence: [DESeq2 bridge report](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/data-preservation-20260930/deseq2-bridge-20261001/REPORT.md)

### Known biology, recovered.

10 / 10 — known PFOA-responsive genes recovered.

On public rat liver toxicology data, the verification rule recovered all ten known PFOA-responsive genes at 2.5 mg/kg and above.

Evidence: [Public toxicology run summary](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/foundation-20261002/workflow-a7/runs/2026-10-21-u31/SUMMARY.md)

### Checked outside the producer.

98 / 98 — verifier tests passed.

An independently implemented verifier recomputes the covered checks with exact rational arithmetic and passes every test in its suite.

Evidence: [Independent-verifier merge validation](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/foundation-20261002/verifier-m1-balance-20261022/MERGE-VALIDATION-20261023.md)

## Depth beneath the results

### Fewer states to certify.

Certificate size. Exclusions that lead to the same analysis are merged: 697 states become 487 and the certificate shrinks by 29.6%.

### The optimum, proved.

Optimality. For fixed discovery tables, the exact best achievable result is derived—and reached.

### Exact conditions for simpler scores.

Method choice. Necessary and sufficient conditions show when a simpler ordered score can replace a four-tier score without losing discoveries.

### Shared rescaling keeps the guarantee.

Preprocessing. Centring and scaling learned from the data and applied to both groups leave the test and its guarantee exactly intact.

### Whole regions, not points.

Interval certification. Interval arithmetic certifies entire regions of continuous parameters, not just sampled values.

### Feasibility before data.

Design. From the design alone, compute the minimum number of discoveries certification can reach—before collecting a sample.

## What is checked

### Check the design before collecting data.

For a declared randomised design, check whether the sample sizes and hypothesis set permit certification. See a design limit early, while the study can still change.

Finite assignment spaces limit attainable p-values and the minimum non-empty discovery count. Passing this preflight is a necessary feasibility check, not a prediction of power or a promise that a certificate will be issued.

### Carry conditions all the way to the claim.

Connect the conditions of each eligible design, preparation and analysis stage to the final claim. Keep the scientific target, assumptions and hypothesis set attached as data move between tools.

One composition result is WT-R v6.3: under the declared finite uniform randomisation law, per-hypothesis inputs imputable under the null (or functions of assignment alone), a fixed hypothesis universe and the declared exact-orbit e-value procedure, e-BH controls FDR at α·K₀/K under arbitrary dependence among hypotheses. K is the fixed number of hypotheses, K₀ the number of true nulls and α the chosen error level. This route uses a sharp null: invariance across assignments of the covered outcome vector. Equality of means alone is not enough for this route.

### Include the exclusions in the check.

Declare the sample-removal family and carry the same exclusions through the supported calculation chain. A stability certificate covers that whole family, rather than a few selected reruns.

Universal deletion stability, a randomisation test of a worst-member statistic, and a direct test of a robust composite null are different claims. In particular, passing an orbit-calibrated worst-member test does not establish that the discovery list survives every deletion.

### Make large checks tractable.

Exploit exact counting and reusable structure where the statistic permits it. Evaluations with specific count-sum statistics returned certified discoveries across thousands of hypotheses.

The reported genome-scale examples use semi-synthetic count data and specific sum-based statistics. Their exact-counting performance is not a runtime guarantee for arbitrary software, every deletion family or every preprocessing pipeline.

### Declare the workflow. Check it independently.

A typed declaration makes the supported design, transformations and decision rules explicit. A separately implemented verifier recomputes the covered checks from that declaration.

The scoped verifier uses exact integer and rational arithmetic for its supported stage language. It checks the record and computation; actual randomisation, the physical invariance of references and declaration-before-outcome chronology also require external evidence.

### Turn uncertainty into a next step.

Return a supported claim with its checking basis, or identify the condition or calculation that needs attention. Make the next useful check clear before a result is carried into a conclusion.

Insufficient design resolution, missing declarations, unmet assumptions, invalid inputs and numerical uncertainty are not evidence of no effect. A safe refusal is also distinct from a runtime failure.

## Match the guarantee to the question

### Design-based route

A guarantee from the assignment.

For eligible randomised designs, the assignment mechanism supplies the reference law. The result described here tests a sharp null—that the treatment changes no unit’s outcome—and connects the declared stages to FDR control without modelling the outcome distribution.

### Model-based research

A guarantee from a sampling model.

The research also includes equal-means nulls for two independent normal samples. That route relies on normality and independent sampling, rather than a sharp null. It remains subject to implementation review and a product-role decision before certificate issuance.

Established scientific tools supply individual analyses and their method-specific
guarantees. The mathematical foundation connects the conditions between stages
and identifies which final claim follows. Each route has its own assumptions
and review status; the design-based result is not the scope of all the research.

## Validation cases

### Check every permitted exclusion.

2,325 — declared deletion cases.

In a compact two-group model, the sign of the final contrast was certified over every removal of up to three of 24 observations. A type-based certificate covered all 2,325 cases with 84 states and passed a separately implemented checker.

Scope: NB profile → changing masked OLS → shared centred prior variance → log-dispersion MAP → original contrast. The claim is the sign of that contrast, over the declared compact model and all admitted global-solution branches. It is neither an arbitrary DESeq2 pipeline certificate nor an FDR result.

Outcome and non-successes: Six original model series with uniform positive oracle signs obtained full-family certificates. Three series with mixed signs were retained as non-successes. The 18 saved runs comprise nine original conditions and nine additional-method runs on those same models, not 18 independent unknown datasets.

Evidence:
- [Scaling-certification report](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/foundation-20261002/scaling-certification-20261020/REPORT.ja.md)

### Certification beyond tiny examples.

15,285 — hypotheses in a count-data evaluation.

Semi-synthetic genome-scale count-data beds produced non-empty certified discovery sets from an 8 + 8 design. Exact counting exploited statistics determined by the treated count sum.

Scope: A bounded evaluation under specified count models and exposure conditions. Full-data sum-law counting is not the cost of all deletion members or a benchmark of arbitrary software. Raw-count, share and reference-ratio nulls must be distinguished from biological expression changes.

Outcome and non-successes: Harder comparison beds also exposed cases where a mathematically valid raw-count guarantee does not control false claims about biological expression. The certified target must therefore be matched to the biological question.

Evidence:
- [Genome-scale results and limits](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/foundation-20261002/workflow-a5d/u30b/RESULTS.md)

### Checks outside the producer.

A separate verifier — a declaration that can be rechecked.

The independent verifier for stage language v2.5 passed 73 conformance tests, with exact rational calculations and explicit refusal of malformed inputs in the covered implementation.

Scope: Finite conformance evidence for that language and verifier version. It is not a test count for the entire product, a proof of arbitrary AI-generated code, a formally verified checker or external expert peer review.

Outcome and non-successes: The verification work included separate implementation and verification roles, defect findings, repairs and re-verification. These were AI-programme checks; the count is implementation evidence, not evidence of detection power.

Evidence:
- [Verifier review and preserved run evidence](https://github.com/licklider-ai/nomue-math-chain/blob/7d94291af4f737869afb76f1528349d1fb7dd02d/lanes/foundation-20261002/verifier-m1-balance-20261022/review-20261024/REVIEW.md)

### Certify a complete continuous domain.

45,260 — certified regions, zero unresolved.

A computer-assisted interval proof established E > 0 over the complete declared real Σd = 2 facet, covering 1,024 initial boxes with 45,260 certified leaves and no unresolved leaves. A separate exact scaling argument established ε₃ > 11/1200 over the full declared Σd ≤ 2 deficit budget.

Scope: The result concerns two intermediate components for the original C4 patterns and six real deficits, under the stated root-identification, exact-arithmetic, Python/Fraction, FLINT/Arb interval-containment and hardware trust. It is not a proof of the final signed Δ, O₁ or C4 conclusion, nor a statistical, real-data or product guarantee.

Outcome and non-successes: The E and ε₃ component obligations are complete in their declared scopes. The signed Δ and full-facet O₁/C4 obligation remains open; positive E and ε₃ alone do not establish it.

Evidence:
- [E full-facet proof and recorded audit](https://github.com/licklider-ai/nomue-math-chain/pull/64)
- [Full-budget ε₃ transfer and review](https://github.com/licklider-ai/nomue-math-chain/pull/78)
- [Open signed-Δ / O₁ follow-on](https://github.com/licklider-ai/nomue-math-chain/pull/109)

## Measured usefulness and trade-offs

N = 16, K = 300, α = 0.1; the 63 main held-out artificial conditions for this sample size. These methods test the declared robust composite null. This is a scoped method comparison, not an end-to-end product benchmark.

| Measure | Perfect separation | Selected two-tier score |
| --- | --- | --- |
| Mean true discoveries | 22.690 | 33.739 |
| Probability of at least one true discovery | 0.817 | 0.604 |

In this comparison, the selected two-tier score increased the average number of true discoveries while reducing the chance of finding at least one. Different research objectives therefore call for different evaluations. This observed trade-off does not establish a mathematical limit on other valid methods.

Fix the method-selection rule under its validity conditions. Choosing the more favourable result after seeing outcomes, or running both at full error level and taking their union, does not automatically retain the FDR guarantee.

The larger artificial study comprised 894 conditions (189 training, 705 held-out).
The displayed rows are only its N=16 main held-out subset, not all 705 conditions.
A separately authored full-output recomputation found no discrepancies in the
stored calculations. Recalculation of fixed synthetic schedules is not
replication in a real-world population or external expert review.

## Research and checking status

WT-R v6.3, the compact-model proofs and the described implementation checks were
reviewed within the AI research programme. This does not claim external expert
peer review or formal verification. Numerical enclosure, statistical validity,
deletion stability and software fidelity remain separately typed claims.
Numerical accuracy alone does not establish statistical validity; a stable
calculation still needs to answer the intended scientific question. FDR bounds
an expectation, not the error fraction in every realised discovery list.

## Established foundations

### Assignment-based exact p-values

For supported randomised designs, derive the reference law—the results chance alone would produce—from the declared assignment mechanism. The calculation must follow that mechanism and the tested null.

### FDR without a correlation model

Valid e-values and e-BH (Benjamini–Hochberg applied to e-values) control the expected false-discovery proportion under arbitrary dependence. Each e-value must be valid for the declared null; FDR is an expectation across repeated studies.

### Numerical bounds that resolve a decision

Enclose numerical error and certify a decision only when the bound separates it from its threshold. Refine or leave the decision unresolved when rounding uncertainty could change it.

### Evidence bound to its version

Keep the declarations, inputs, method and execution identity, checked conditions, results and supported claims together. The Record makes the checking basis inspectable and preserves it when the study changes.

- [Randomisation tests and their conditions](https://arxiv.org/abs/2203.10980) — Zhang & Zhao.
- [False discovery rate control with e-values](https://arxiv.org/abs/2009.02824) — Wang & Ramdas.
- [E-values: calibration, combination, and applications](https://arxiv.org/abs/1912.06116) — Vovk & Wang.

These references support the existing foundations, not independent validation of
SciGround's own implementations or a claim that the underlying methods were
invented by SciGround.