# Executable example and observed evidence

The example demonstrates a failure of statistical composition while every individual feature comparison can be computed correctly.
It also measures what a proof and runtime specification add beyond conventional tests.

## Exact counterexample

Eight units receive four treatments, giving 70 assignments.
The fixed feature panel contains one binary vector from each complementary assignment pair: 35 features.
The entire matrix is fixed before assignment, satisfying the example's global sharp-null construction.

For every observed assignment, one feature perfectly separates the groups.
Its absolute scaled mean difference is 16.
Freezing that observed winner gives only two equally extreme assignments, so the reported p-value is `2/70 = 1/35`.
At alpha `1/20`, the procedure rejects for every assignment: a 100% false-rejection probability.

When selection is rerun, every assignment has some perfectly separating feature.
The maximum statistic is therefore 16 throughout the assignment space.
Its p-value is 1, giving no rejections.
The [actual input matrix](../results/adversarial-data.json) and both R output files are retained.

This intentionally adverse panel is a proof-of-failure example, not a model of typical biological data.
The corrected global test does not imply that the winning gene is individually non-null.
Strong family-wise control under partial nulls, selective p-values, and FDR require separate arguments.

## External panel selection remains an assumption

The independent audit selected the observed winning feature before calling the checker, then supplied only that column.
Every one-column table is computed correctly for its supplied panel.
Across all 70 observations, every check can accept while the selected observed p-value is always `1/35`.
The original global-null rejection probability is again 100%.

The revised experiment reproduces that boundary on all 70 assignments.
A truthful `selected_using_observed_assignment` history is refused in all 70 cases.
A false fixed-panel declaration still passes in all 70 cases.
Recording history makes the premise visible; it cannot prove the premise.
See [external-selection results](../results/external-selection-boundary.json).

The checked scope is the supplied-panel maximum statistic and its ranks.
It does not include arbitrary panel construction, adaptive preprocessing, or historical independence of panel selection.

## Less structured synthetic count matrices

The experiment generates 100 Poisson and 100 gamma-Poisson matrices, each with eight units and 100 features.
Each generated matrix is then held fixed, and all 70 assignments are enumerated.
These are exact conditional rejection fractions averaged over the generated matrices.
There is no Monte Carlo error from sampling assignments.
The matrix generators and seeds are in `experiments/run.py`; no real biological data were used.

| Fixed-matrix generator | Full-selection global test | Frozen selected feature | Matrices with frozen error above 5% |
| --- | ---: | ---: | ---: |
| Poisson, 100 matrices | 41/1750 = 2.343% | 47/175 = 26.857% | 100/100 |
| Gamma-Poisson, 100 matrices | 47/1750 = 2.686% | 93/500 = 18.600% | 100/100 |

All correct conditional rejection fractions stayed below 5%.
Complement symmetry makes each nonempty rejection set contain at least two assignments.
At alpha 5%, at most three of 70 assignments could reject, but symmetry forces an even count.
The effective ceiling is therefore `2/70 = 2.857%`; correct fractions here are either 0 or `1/35`.
The observed 2.3–2.7% averages reflect this discreteness, not general near-5% calibration.
These summaries are descriptive results from fixed seeds. They do not estimate prevalence or error rates of deployed bioinformatics workflows.
See [summary results](../results/statistical-results.json) and [all 200 matrix results](../results/count-matrix-rejection-fractions.json).

## Proof and bounded checks

The Lean theorem holds for every finite natural-number score list and every natural threshold numerator.
It includes arbitrary ties and duplicate score occurrences.
The transitive axiom report contains only `propext` and `Quot.sound`.
A strict-tail mutation fails to establish the same theorem.
For example, a one-element list with strict rank zero would reject one outcome at threshold zero.

The compiled executable uses the same `rank` definition as the theorem.
Its numerical outputs matched Python on all 3,279 score vectors of lengths 1–7 over `{0,1,2}`.
That comparison checks execution correspondence on a bounded domain; the Lean counting theorem itself is unbounded in list length and values.

An additional exhaustive check covers all 4,096 binary matrices of shape 6×2 and all 20 balanced assignments.
At alpha 10%, the correct method's largest rejection fraction was 10%.
Frozen selection reached 20%, exceeding 10% in 360 matrices.
See [finite-check results](../results/finite-checks.json).

The theorem does not prove the Python enumerator, wrapper, R implementation, or probability model.
No independent proof-checker run was performed beyond the installed Lean kernel check.
Compiler, runtime, parsers, and operating system remain trusted.

## Comparison with conventional testing

The [protocol](experiment-protocol.md) fixes two ordinary fixtures and 42 strong reference fixtures.
The latter include multiple features, ties, and blocked assignments.
Eight mutation classes were evaluated on all 42 fixtures for the strong and runtime-check arms.
These were authored in the same research session. The comparison was not blinded or independently preregistered.

| Seeded defect | Ordinary fixtures | Strong independent differential tests | Per-run specification checker |
| --- | :---: | :---: | :---: |
| Strict `>` tail instead of inclusive `>=` | Caught | Caught | Caught |
| Drop an assignment | Caught | Caught | Caught |
| Freeze observed winning feature | Missed | Caught | Caught |
| Incorrect denominator | Caught | Caught | Caught |
| Ignore the declared blocks | Missed | Caught | Caught |
| Replace one assignment with a duplicate | Missed | Caught | Caught |
| Change a score | Caught | Caught | Caught |
| Wrong input identity | Missed | Caught | Caught |
| Correct producer | Accepted | Accepted | Accepted |

Ordinary fixtures caught 4/8; strong tests and runtime checks each caught 8/8.
No correct output was refused across the 42 comparison fixtures.
The result supports no claim of greater defect detection than strong testing.
See the complete [failure counts and diagnostics](../results/assurance-comparison.json).

The proof contributes universal coverage of a precise rank property.
The runtime checker checks each received supported output, including inputs outside the test corpus.
Both remain limited by specification meaning and implementation trust.
An independent reference implementation offers substantial practical assurance and may be cheaper for some workflows.

## R/Python/Lean bridge

Three actual correct R outputs passed: the adversarial panel, a blocked design, and a random count matrix.
The actual frozen-selection R output was refused.
The [R correspondence record](../results/r-correspondence.json) binds input/output bytes and core, producer, verifier, bridge, and contract hashes.
Receipts explicitly describe a hypothetical assignment table and carry no observed assignment.
A separate observed-study interface would need a checked observed assignment and its corresponding p-value.
The archive contains the same byte snapshots consumed and checked by the adapter.

The bridge tests reproduced a real same-byte decoder discrepancy:
Python's default decoder returns 2 for `{"x":1,"x":2}`; R/jsonlite's named lookup returns 1.
The strict adapter rejects duplicate keys at every object depth before R execution and when reading R output.
It also rejects floating-point numeric tokens, NaN, and malformed contract values.

Each R invocation uses a fresh private directory.
Each Lean invocation separately uses a fresh private directory and a natural-number CSV file.
Eight concurrent R/Lean invocations passed with distinct input identities and correct output correspondence.
A public-path replacement test confirmed that a previously captured byte snapshot remains the executed input.
These are concurrency and boundary tests, not a proof against a hostile process or compromised host.

## Build identity and independent-review status

The first independently reviewed version had no executable-identity gate.
The auditor's retained summary reports acceptance with a different core executable.
That finding concerns a wrong trusted artifact, not a counterexample to the audited theorem or its original executable.

The revised core path requires a successful-build manifest matching the current proof sources, build recipe, and executable.
It checks that manifest before and after invocation. Receipts bind the manifest as well.
The local build process and unsigned manifest are trusted; this is not cryptographic attestation against a malicious owner.

Earlier independent work reproduced the theorem, scientific outputs, 11 tests, and a byte-identical core rebuild.
The later audit stopped because of a platform security restriction.
Its blocked action was not rerouted or retried here.
The revised selection-history contract, implementation-bound receipts, build gate, and twelfth boundary test have owner validation only.
They have not received independent re-review.

## An assumption violation that passes every arithmetic check

Use one binary feature with four zeros and four ones.
The valid uniform design rejects two of 70 assignments, giving probability `1/35` at alpha 5%.
Now suppose the actual assignment mechanism puts probability `9/20` on each rejecting assignment.
Allocate the remaining `1/10` across the other assignments.
The identical correct p-values now reject with probability `9/10`.

The checker accepts the computation because it matches the declared uniform law.
No byte check or rank proof can establish that the real experiment followed that declaration.
The example isolates a scientific premise that must remain visible to the reviewer.

## Runtime cost

Local medians from five repetitions include Lean process startup in the checker path.
These measurements use CPU execution and bounded synthetic inputs.
They are not production or GPU benchmarks.

| Units × features | Assignments | NumPy producer | Independent Python reference | Python checks plus Lean core |
| --- | ---: | ---: | ---: | ---: |
| 6×20 | 20 | 0.233 ms | 0.683 ms | 35.300 ms |
| 8×100 | 70 | 0.771 ms | 11.603 ms | 45.966 ms |
| 12×200 | 924 | 11.595 ms | 362.845 ms | 472.355 ms |

The wrapper is materially slower than the small producer.
Absolute overhead remains below one second in these cases, but this does not establish acceptable production throughput.
The final native core is approximately 6 MB after removing an unused compiler import.
Its clean rebuild and build manifest were byte-identical under the recorded toolchain.
The rank implementation is quadratic in assignment count. Exhaustive assignment enumeration also grows combinatorially.
Certified reuse, efficient ranking, and Monte Carlo procedures each need additional reasoning before expansion.
See [benchmark data](../results/benchmark.json).

## A credible next comparative study

The present experiment establishes mechanics and failure modes. It cannot establish product-level superiority.
A stronger study should use these rules:

1. Recruit independent statistical and implementation reviewers when authorized.
2. Freeze 10–20 real analysis variants with specific nulls, estimands, and integration paths.
3. Include resampling with learned preprocessing, one selected-inference method, and one final-set reporting workflow.
4. Use authentic historical regressions and independently authored mutants; keep a held-out portion undisclosed.
5. Give conventional testing strong property, metamorphic, differential, and calibration tools under the same maintenance budget.
6. Give the assurance arm the same baseline tests plus a fixed specification/proof budget.
7. Count claim-changing defects, correct refusals, incorrect refusals, annotation time, repair time, and runtime/storage overhead separately.
8. Evaluate scientific premise violations as a distinct category; no tool earns credit for detecting unverifiable truth from a declaration.
9. Test mismatched bytes, duplicate fields, coercions, reordered identities, stale artifacts, and concurrent execution independently of statistical errors.
10. Have a reviewer judge whether the specification still answers the intended scientific question.

Primary endpoint: incremental detection of consequential held-out defects per unit of maintenance effort, with valid-workflow refusal rate reported beside it.
Secondary endpoints: change resilience, supported workflow fraction, user comprehension of assumptions, and actual execution coverage.
Report both successful and unsupported examples.

Proceed only if the formal layer supplies repeatable benefit beyond a strong conventional baseline or materially reduces repeated review effort.
The current 8/8 tie leaves that business question open.