Proofs & surfaces

This section is the proof side: how end-user theorems are shaped, the conventions for writing them, and the bookkeeping that keeps the artifact honest.

In this section

• Theorem surfaces — the top-level shapes (ComputeCorrect.Realizes_without_Rounding, ComputeRefine.Realizes, and friends) that kernels and specs are expressed against.

• Correctness surfaces — surface-by-surface guide for picking the right one for a given kernel/spec relationship.

• Proof conventions — naming, structure, invariant placement, and the patterns that recur across the bench corpus.

• Approx-GELU φ strategy — the specific numerical-approximation proof strategy used for the GELU / φ family.

• Kernel manifest — what the manifest tracks, the schema, and how CI uses it to detect drift.

• Trust audit — axiom dependencies, statements, and specification checks.