Document KitchenSpeak trusted-base postulates (governance: trusted-base policy)

Annotate every Agda postulate with a leading AXIOM: comment and enumerate
them in PROOF-NEEDS.md, satisfying the trusted-base reduction policy.
These postulates are deliberate trust boundaries (postulated sensor
oracles + the GENTLE controller spec), not undocumented escape hatches.

Author: claude

PROOF-NEEDS.md

@@ -21,6 +21,21 @@
 | Tangle Lean proofs | Extend Tangle.lean coverage | Existing Lean proofs are partial |
 | Oblibeny ABI | Extend Interface.idr with full package proofs | Current ABI is minimal |
 
+## KitchenSpeak Trusted Base (Agda postulates)
+
+KitchenSpeak's proofs are deliberately built on a small, explicit trusted
+base: the *postulated echo-oracles* (sensors) and the GENTLE *controller
+spec*. These are not soundness gaps to close but documented trust
+boundaries (see each proof's final section and `COMMENTARY.adoc §Echo`).
+A production lowering replaces each with a verified HAL binding.
+
+| Postulate | File | What it trusts | Production replacement |
+|-----------|------|----------------|------------------------|
+| `viscosity-at` | `kitchenspeak/proofs/agda/Dough.agda` | Torque sensor stream | Verified HAL torque binding |
+| `temp-at` | `kitchenspeak/proofs/agda/PoachedEgg.agda` | Hob thermometer stream | Verified HAL thermal binding |
+| `white-set-at` | `kitchenspeak/proofs/agda/PoachedEgg.agda` | Visual albumen classifier | Verified/empirically-bounded classifier |
+| `gentle-bounded` | `kitchenspeak/proofs/agda/PoachedEgg.agda` | GENTLE controller never overshoots target cap | Integrator bound on the slope |
+
 ## Recommended Prover
 
 **Coq** for Ephapax (existing proof infrastructure). **Lean4** for Tangle (existing). **Idris2** for ABI layers. **OCaml** extraction from Coq for AffineScript type checker verification.

kitchenspeak/proofs/agda/Dough.agda

@@ -175,7 +175,12 @@ bind-dough _ _ = mkDough KNEADABLE
 -- *assumes* its values exist and discharges the surrounding control
 -- flow. See COMMENTARY.adoc §Echo for the discussion of postulated
 -- oracles and the proven/postulated boundary.
-
+--
+-- AXIOM: postulated echo-oracle (the torque sensor stream) — the
+-- physical world, not a derivable term. The proof trusts the sensor
+-- and discharges the surrounding control flow; a production lowering
+-- replaces it with a verified HAL binding (§8(a)). Trusted base
+-- contribution: 1 sensor postulate.
 postulate
   viscosity-at : Minutes → Torque-dNm
 

kitchenspeak/proofs/agda/PoachedEgg.agda

@@ -163,7 +163,13 @@ record Vinegar : Set where
 --   temp-at        — the hob thermometer, in °C, sampled per minute.
 --   white-set-at   — the visual albumen-coagulation classifier; reports
 --                    a coagulation score, "set" once it crosses 1.
-
+--
+-- AXIOM: these are postulated echo-oracle sensor streams — the physical
+-- world, not derivable terms. The proof trusts the classifier pipeline
+-- and discharges the surrounding control flow; a production lowering
+-- replaces each with a verified HAL binding. This is the deliberate
+-- proven/postulated trusted-base boundary (COMMENTARY.adoc §Echo; §9(a)
+-- below). Trusted base contribution: 2 sensor postulates.
 postulate
   temp-at      : Minutes → Celsius
   white-set-at : Minutes → ℕ
@@ -234,7 +240,11 @@ poach e v (suc n) t with white-set-at t ≥? set-threshold
 -- analogue of the sensor postulate — it is the controller's contract,
 -- supplied by the HAL, not derived here. A production lowering proves
 -- it from an integrator bound on the slope.
-
+--
+-- AXIOM: the GENTLE controller's specification, supplied by the HAL and
+-- trusted here rather than derived. A production lowering discharges it
+-- from an integrator bound on the slope (§9(b)). Trusted base
+-- contribution: 1 controller postulate.
 postulate
   gentle-bounded : ∀ (t : Minutes) → temp-at t ≤ target-cap