# Human-readable contract: exact global randomization test

| Field | This example |
| --- | --- |
| Question | Does treatment affect any measured feature in this fixed panel? |
| Null | Every unit has the same feature vector under every allowed assignment. This is the global sharp null. |
| Design | Treatment is uniform over all assignments satisfying each declared block's fixed treated count. |
| Statistic | For each assignment, take the largest absolute, scaled treated-versus-control mean difference across all features. |
| Selection | Recompute the winning feature within the supplied panel for every assignment. Record the panel-selection history separately. |
| P-value | Count all assignment statistics at least as large as the observed statistic. Divide by the complete assignment count. |
| Claim | Under the stated design and null, the probability of rejection is at most the chosen threshold. |
| Assumptions | The real assignment law matches the declaration. The supplied panel and algorithm are fixed across assignments. Measurements and identities are correct. |
| Implementation | R or Python produces scores and ranks. A Python wrapper recomputes scores. A compiled Lean definition recomputes inclusive ranks. |
| Limits | No selected-gene, partial-null, weak-average-effect, FDR, observational-exchangeability, or biological-mechanism guarantee. |
| Refusal | Unsupported claim/design, unknown or declared adaptive panel history, malformed identities, duplicate keys, or mismatched scores/ranks. |

The output is a hypothetical assignment table, not an observed-study p-value receipt.
Every receipt sets `artifact_role = hypothetical_assignment_table` and `observed_assignment = null`.
It records the selection-history declaration and sets `history_verified = false`.
Only the supplied-panel maximum statistic is checked. Arbitrary adaptive preprocessing is not verified.

The null is a hypothesis being tested. It is not an empirical assumption that must be declared true before testing.
The assignment mechanism and the fixed analysis procedure are substantive premises needed for the error bound.

`panel_history.status` must be `declared_fixed_over_assignments`, with a nonempty human-readable `basis`.
Declared observed-assignment selection and unknown histories are refused.
A false fixed-panel declaration can still pass. The adapter cannot establish historical truth from an attestation.
The experiment retains this counterexample explicitly in `results/external-selection-boundary.json`.

## Exact specification

Let `X[i,g]` be nonnegative integer counts, with named units and features.
Let `Ω` contain every binary assignment satisfying the declared block counts, exactly once.
Let `N = |Ω|` and `m` be the total treated count, which is fixed across `Ω`.

```text
D_g(X,z) = abs((n-m) * sum_{i:z_i=1} X[i,g]
                 - m * sum_{i:z_i=0} X[i,g])
T(X,z)   = max_g D_g(X,z)
r_z      = #{w in Ω : T(X,w) >= T(X,z)}
p_z      = r_z / N
```

`D_g` is `m(n-m)` times the absolute mean difference. This common positive factor preserves ordering.
The two-sided construction uses an absolute statistic and one inclusive upper tail.
It does not adopt every library's convention for doubling a one-sided p-value.

The supported domain is 2–12 units, 1–200 features, and counts from 0 through 1,000,000.
Each block must contain both treatment and control units. Enumeration is limited to 2,000 assignments.
No missing values, weights, nuisance regression, random preprocessing, or Monte Carlo sampling are supported.

## What is proved

For every finite list `xs` of natural-number scores and every natural `k`, Lean proves:

```text
#{s occurring in xs : #{t occurring in xs : s <= t} <= k} <= k
```

Occurrences count separately, including ties. See `Resampling.finite_rank_bound` in `formal/Rank.lean`.
Its proof chooses the smallest score among rejected occurrences.
Every rejected occurrence lies in that score's inclusive upper tail, whose size is at most `k`.

For a uniform index in a nonempty list, divide this bound by `N`.
For a threshold `alpha`, set `k = floor(alpha*N)`.
This gives `Pr(p <= alpha) <= floor(alpha*N)/N <= alpha`.
This probability interpretation is a mathematical argument here; Lean checks the finite counting theorem.

Under the global sharp null, `X` is fixed while assignment varies.
A fixed deterministic procedure therefore produces one common score list across possible observed assignments.
Freezing an observed winner produces different comparison lists for different observations. The theorem no longer supplies that procedure's guarantee.

## Implementation correspondence and trust

| Edge | Evidence here | Remaining trust |
| --- | --- | --- |
| Source bytes → decoded contract | Strict UTF-8 JSON decoder rejects duplicate keys, noninteger numeric tokens, and unsupported fields | Python parser and validation code |
| Contract → assignment space | Independent bit-vector enumeration checks producer combinations and R enumeration | Python enumeration; not formally proved |
| Matrix/assignment → statistic | Exact Python sums check each R/Python output score | Python wrapper; not formally proved |
| Score vector → ranks | The compiled core executes the same Lean `rank` definition used by the theorem | Lean compiler/runtime, C compiler, parser, OS/hardware |
| R execution → accepted output | One input snapshot, private directory, one output snapshot, hashes, and per-run comparisons | R/jsonlite and truthful runtime execution |
| Uniform score index → scientific error claim | Finite mathematical argument under the declared randomization and global null | Actual design, panel/algorithm selection history, measurements and meaning |

The bridge passes unique-key JSON to R and comma-separated natural numbers to Lean.
All supplied values stay below exact integer limits for NumPy int64 and R doubles.
The `n² * MAX_COUNT < 2^53` guard is conservative for the scaled statistic.

A receipt binds the core binary, Lean sources, R producer, Python verifier/bridge/entry point, and this contract by SHA-256.
Those artifacts must remain unchanged during the invocation.
The core checks a successful-build manifest against the current Lean sources, build recipe, and executable before and after invocation.
A missing or mismatched build record is refused. Receipts also bind that build record.
The build recipe and unsigned manifest remain trusted; deliberate joint replacement is outside this guarantee.
Hashes alone do not prove a source-to-binary build relation.

A receipt records accepted numerical correspondence. It is not a kernel proof of that dataset.
The Python checker, R program, serialization, and full scientific procedure are not formally verified.
Hashes bind bytes; they do not establish authenticity or an honest assignment mechanism.
Private files prevent collisions among cooperating invocations. They do not protect against a compromised operating system.

## Safe reuse rule to investigate next

A preprocessing result may be reused across assignments when it is invariant over the declared assignment space.
Otherwise, rerun it inside each assignment, or provide a different valid conditional-inference construction.

Dependency tracking can conservatively identify label-dependent computation. It cannot prove a data-generating distribution.
Label-blind preprocessing can be safe for this conditional randomization test without establishing independence for a separate parametric test.