audit: classify 4 PA021 justified real-analysis postulates (information_theory.agda)

audits/assail-classifications.a2ml

@@ -0,0 +1,26 @@
+;; SPDX-License-Identifier: MPL-2.0
+;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+;;
+;; Assail Classifications — standards
+;; See panic-attack/.claude/CLAUDE.md § "User-Classification Registry".
+
+(assail-classifications
+  (metadata
+    (version "1.0.0")
+    (project "standards")
+    (last-updated "2026-05-26")
+    (entries 1)
+    (status "active"))
+
+  ;; ─── PA021 ProofDrift — justified postulates (real-analysis) ─────────────
+  ;; lol/proofs/theories/information_theory.agda has 4 postulates whose proofs
+  ;; would require a real-analysis formalisation in Agda (e.g. over ℝ). The
+  ;; file's own comment at line 111-112 explicitly classifies them:
+  ;; "Classified as justified postulates, not proof debt."
+
+  (classification
+    (file "lol/proofs/theories/information_theory.agda")
+    (category "ProofDrift")
+    (classification "justified-postulate-real-analysis")
+    (audit "audits/audit-pa021-justified-postulates-2026-05-26.md")
+    (rationale "4 information-theory postulates (entropy-nonnegative, kl-nonnegative, js-symmetric, js-bounded). Each has a textbook proof (HoTT/Gibbs/Lin 1991) but requires real-analysis formalisation in Agda over ℝ. File-internal comment explicitly classifies these as justified postulates, not debt.")))

audits/audit-pa021-justified-postulates-2026-05-26.md

@@ -0,0 +1,43 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
+# Audit: justified real-analysis postulates (PA021)
+
+**Auditor**: Jonathan D.A. Jewell
+**Date**: 2026-05-26
+**Scope**: 1 PA021 ProofDrift finding covering 4 postulates in `lol/proofs/theories/information_theory.agda`.
+**Cross-reference**: campaign tracker [hyperpolymath/panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32).
+**Registry**: `audits/assail-classifications.a2ml`.
+
+## Context
+
+`lol/proofs/theories/information_theory.agda` contains 4 postulates:
+
+1. `entropy-nonnegative : ∀ {n} (d : Distribution n) → entropy d ≥ 0.0` — follows from `-p·log(p) ≥ 0` on `0 ≤ p ≤ 1`.
+2. `kl-nonnegative : ∀ {n} (p q : Distribution n) → kl-divergence p q ≥ 0.0` — Gibbs' inequality / log-sum inequality.
+3. `js-symmetric : ∀ {n} (p q : Distribution n) → jensen-shannon p q ≡ jensen-shannon q p` — follows from symmetry of KL terms in the midpoint construction.
+4. `js-bounded : ∀ {n} (p q : Distribution n) → 0.0 ≤ jensen-shannon p q × jensen-shannon p q ≤ 1.0` — Lin 1991; upper bound via Jensen's inequality.
+
+The file's source-internal comment at line 111-112 reads:
+
+> proofs would require a real-analysis formalisation (e.g. over ℝ). Classified as justified postulates, not proof debt.
+
+Each statement has a textbook proof, but discharging them in Agda requires:
+
+- A real-analysis library formalising ℝ as a Cauchy/Dedekind-complete ordered field
+- Log / exp / Jensen's-inequality lemmas
+- Probability-distribution structures (likely via `Vec` of reals summing to 1 with positivity)
+
+This is a substantial library-development effort orthogonal to the standards repo's purpose. Per the file's own classification, these are **justified postulates** — known-true theorems from classical information theory whose Agda formalisation is out of scope.
+
+## Anti-gameability
+
+The registry is `audits/assail-classifications.a2ml`. The classification covers only this specific file; any new postulate in another proof file remains visible. Additional postulates added inside `information_theory.agda` would require updating both this audit doc and the rationale, both visible in the diff.
+
+## Verification
+
+No proof source touched; `agda --check` rebuild is moot (input unchanged from main).
+
+Refs hyperpolymath/panic-attack#32.