# Human-readable statistical contract

## Input and fixed scope

- A finite set of possible outcomes, represented as a list with nonnegative rational weights summing to one. Repeated world entries simply combine their weights.
- One hypothesis family and one alpha fixed across those outcomes. Operational use has distinct stable IDs and `0 < alpha < 1`; the mathematical proof also handles alpha zero and an empty true-null subset.
- For each outcome and hypothesis, the **actual supplied** rational p-value. The prototype's accepted inputs lie in `[0,1]`; the probability proof itself only needs nonnegativity.
- An arbitrary fixed subset of true null hypotheses. It represents the underlying truth, not labels guessed by the analyst. The theorem quantifies over every such configuration.
- Marginal validity for each true null: for every nonnegative rational threshold `t`, the total weight of outcomes with `p_i ≤ t` is at most `t`. It is sufficient to establish this at `alpha/m0`, but full super-uniformity is the normal reusable premise.

There is **no independence or positive-dependence assumption**. Non-null p-values can have any nonnegative distribution and depend on the null values. No information about the unknown true-null subset is required by the algorithm.

## Procedure and conclusion

The procedure uses exactly the frozen rank formula:

```text
q_i = min(1, max over p_j <= p_i of
             (m - number of p_k < p_j) * p_j)
reject_i iff q_i <= alpha
```

Under the premises above, the total probability weight of outcomes in which at least one true null is rejected is at most alpha. This is **strong FWER control in the finite rational model**, since any fixed truth configuration is allowed.

`rejection_implies_small_true_null` proves the deterministic step. Pick a minimum true-null p-value. If any true null is rejected, its candidate prefix includes the minimum's term. At least `m0` hypotheses remain at that minimum, so `m0 × p_min ≤ alpha`. Thus a false rejection implies some true-null p-value is at most `alpha/m0`. `mass_any_le_sum` proves the finite union bound directly from nonnegative weights; marginal validity then gives `m0 × alpha/m0 = alpha`. The empty true-null case has probability zero.

`frozen_formula_eq` is definitional equality with the frozen prototype's `holmSpec`. `holm_map` proves that constructing rows from fixed hypothesis indices preserves the formula. `frozen_formula_fwer` expresses the probability result using that original function. It does not rely on an unproved equivalence to an unrelated sorting implementation.

`checked_reporting_fwer` further uses the original `check_sound`: when the checker accepts, the reported row decision equals the formula. For arbitrary candidate values and flags, the event “accepted and a true-null rejection reported” is contained in the formula's false-rejection event. Failed checks report no rejections, so this subset retains the same unconditional bound. This corollary does **not** require every possible candidate to pass.

## What a human must justify

A scientific owner or reviewer must record:

1. **Hypothesis and family definition.** What each ID means, which comparisons belong to the reported error claim, and when that family and alpha were fixed. Each formal index must continue to denote the same scientific hypothesis; row strings and metadata must preserve that meaning.
2. **P-value validity rationale.** The sampling/randomization model, statistical test, calibration result and assumptions supporting super-uniformity for a true null. This concerns the values actually passed to the checker, including finite-precision transformations. A small observed p-value, a software name or a successful adjustment is not that rationale.
3. **Selection and repetition.** Whether genes, models, contrasts, preprocessing choices or repeated analyses were chosen using these data. If the family is random, supply an appropriate conditional-validity argument or a selection-adjusted procedure; the fixed-family theorem is not enough by itself. Optional stopping or repeated testing must already be covered by the p-value law or by a different error-spending contract.
4. **Reporting behavior.** Only accepted decisions are reported; failed checks do not fall back to unchecked results. Do not condition the error-rate claim on runs that passed, on significant results, or on a selectively published subset.
5. **Model applicability and execution.** Whether a finite rational law is actually justified, or whether the general measure-theoretic extension is needed; correct data/ID binding; and the declared parser, adapter, compiler and runtime trust.

The human is not asked to identify which nulls are true. They must justify the method's validity when a null is true. An attestation records the rationale and its owner; it does not manufacture a mathematical premise.

## Exclusions and refusal

This theorem does not prove DESeq2 calibration, biological truth, causal interpretation, data provenance or experimental validity. It does not establish arbitrary real-valued probability spaces, probability of a hypothesis being true, FDR, or per-run posterior error risk. It does not prove the native compiler, parser or Python/R transport. The gate theorem covers the pure Lean checker; using the executable retains the prototype's declared trust boundary.

If the family, validity rationale, model applicability or report policy is missing, retain the computational result's actual status but mark the **statistical guarantee unsupported for that use**. Do not silently treat a selected family as fixed, spend alpha again on each chunk, or describe kernel-checked formula agreement as established calibration.