# Deployment contracts and evidence gates

This document separates assumptions from accomplished checks. A Boolean setting
in the simulator is NOT evidence that a real deployment enforces the setting.

## Threat model

The adversary controls the untrusted worker's proposals, equivalent encodings,
completion/withholding choices, private timing, bounded heat-generating workload,
and attempts at direct egress or shared-resource signaling. It may know the
entire design, plan arbitrarily well, collaborate with other workers, and adapt
to previous public observations. Multiple colluding workers must be modeled as
one adversary with an aggregate load bound; the single-worker bound must not be
reused without accounting for their combined actuation.

The receiver sees precisely the public release transcript, the modeled shared
resource/network coordinates, and the mediated thermal-health symbol. There is
no uncontrolled nearby receiver with raw analog sensors. All externally readable
logs, billing, fan behavior, radio emissions, acoustics, light, clock effects,
and thermal throttling must either be excluded by a justified deployment
contract or added as observation channels. This bundle does not show that they
have been excluded on any real machine.

## Required contracts

1. **Authorized result and public schedule.** The task and declassification policy
   are selected outside the untrusted worker. Raw proofs, stylistic variants,
   diagnostics, and provenance chosen by the worker are not released. Canonical
   payload size may depend on already-public data; unauthorized-dependent lengths
   are forbidden.
2. **Sound bounded verification and total fallback.** A private verifier accepts
   only the canonical authorized answer. A trusted independently sufficient path
   produces that same answer within the fixed public deadline even when the worker
   withholds, crashes, floods invalid proposals, or exhausts its own quota.
3. **Persistent timing/resource isolation.** Completion time, proof-checking work,
   fallback work, power saving, and retries do not affect any other observable
   workload. Fixed application timestamps alone are insufficient.
4. **Complete I/O mediation.** No direct network, package-manager communication,
   telemetry, writable shared storage, or diagnostic side path bypasses the gate.
5. **Thermal envelope and sensor mediation.** The stipulated a, b, load,
   disturbance, initialization, and threshold bounds hold for every accepted
   deployment state. Raw sensor access and indirect effects cannot circumvent
   the observation map. Sensor/clock virtualization must be enforced below the
   untrusted component, not requested in its prompt.
6. **Trusted boundary integrity.** The worker cannot rewrite the release policy,
   checker, control firmware, proof state, cost model, signed configuration, or
   evidence gates. Hardware operates within the specified envelope.

## Promotion gates

| Gate | Current publication status |
|---|---|
| Exact search replay | Passed |
| Original global integer optimality certificate | Passed by algebraic derivation and exact arithmetic checker |
| Independent bounded search for cheaper candidates | Passed |
| Digital ablation counterexamples | Passed |
| Thermal near-miss and all 55 default design-pair classifications | Passed |
| Unit tests | 34 passed |
| Python syntax/bytecode compilation | Passed |
| Lean elaboration and kernel checking | Passed with pinned Lean 4.19.0 |
| Lean axiom audit | 24 public theorems; standard `propext`, `Quot.sound` only |
| Real-valued physical model to integer envelope formal refinement | NOT COMPLETED |
| Concrete gate implementation to abstract specification | NOT COMPLETED |
| Real hardware parameter envelope | NOT MEASURED |
| Complete real observer/actuator inventory | NOT VALIDATED |
| Real deployment best-practice designation | NOT EARNED |

There is no authorized promotion to production in this bundle. Failed or missing
proof gates must not be represented as successful validation. A model mismatch is
not evidence that mathematical configuration synthesis is futile; it is a
specific obligation to repair the model or implementation.

## What this does not prove

Confidentiality does not by itself prove safety of authorized actions, good
objectives, resistance to arbitrary physical compromise, or useful operation on
all open-ended AI tasks. An allowed output can still be dangerous without being
a covert channel. Integrity and action-safety properties need their own theorem
statements. Fully compromised receiver hardware with raw sensors is outside the
present quantized-observation theorem.