// SPDX-License-Identifier: CC-BY-SA-4.0
= LOL Information-Theory Postulate Audit
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
:updated: 2026-04-05
:target: lol/proofs/theories/information_theory.agda

== Summary

`information_theory.agda` contains **9 postulates**. Audit verdict:

- **4 are legitimate FFI axioms** (float arithmetic bridged to runtime)
- **4 are theorems that SHOULD be proven** (currently postulated)
- **1 is a relation declaration** that should move to imports

== Per-postulate verdict

[cols="3,2,3,3",options="header"]
|===
| Postulate | Line | Verdict | Action

| `log₂ : Float → Float`
| 47
| ✓ FFI axiom
| Keep. Foreign float operation.

| `_*f_ : Float → Float → Float`
| 48
| ✓ FFI axiom
| Keep. Foreign float multiply.

| `_+f_ : Float → Float → Float`
| 49
| ✓ FFI axiom
| Keep. Foreign float add.

| `negateF : Float → Float`
| 50
| ✓ FFI axiom
| Keep. Foreign float negate.

| `_/f_ : Float → Float → Float`
| 67
| ✓ FFI axiom
| Keep. Foreign float divide.

| `entropy-nonnegative`
| 103
| ✗ Provable
| Replace with constructive proof. Each `plogp p` is either 0 or `-p·log₂(p)` where p∈[0,1] means log₂(p)≤0, so `-p·log₂(p)≥0`. Sum of non-negatives is non-negative. Requires float lemmas about `log₂` on [0,1]; add those as auxiliary postulates (honest FFI layer) but the top-level theorem should be proven.

| `kl-nonnegative`
| 109
| ✗ Provable
| Gibbs' inequality is a classical theorem. Proof uses Jensen's inequality on the convex function `-log`. Standard proof strategy: log-sum inequality, or expand via `x log(x/y) ≥ x - y`. Should be proven from standard real-analysis lemmas.

| `js-symmetric`
| 115
| ✗ Trivially provable
| By construction, JSD(P,Q) = (D(P‖M) + D(Q‖M))/2 where M = (P+Q)/2. Swap P↔Q gives the same M, so JSD(Q,P) = (D(Q‖M) + D(P‖M))/2 = JSD(P,Q). Proof is 2-3 lines in Agda.

| `js-bounded`
| 120
| ✗ Provable (with effort)
| Upper bound JSD ≤ log(2) requires the information-theoretic log-sum inequality. Non-trivial but classical. Should be proven or imported from an existing Agda library.
|===

== Additional concerns

- **`_≥_` and `_≤_` declared as local where-clauses** (lines 104-105, 110-111, 121-123). These should be imported from `Data.Float.Properties` or defined module-wide, not per-postulate. Current structure means each postulate's `_≥_` is a distinct, empty relation — any value satisfies it vacuously. This is a **correctness bug**: the postulates are trivially satisfiable because the order relation is unconstrained.

- **License header**: MIT AND LicenseRef-Palimpsest-0.8 (not the newer PMPL-1.0-or-later). Acceptable given attributed third-party origin (Ehsaneddin Asgari).

== Remediation plan

=== Phase 1 — fix the order relation bug (HIGH priority)

Replace the where-clause declarations of `_≥_`/`_≤_` with a module-level import
from a float-comparison library. Without this, the theorem statements are
vacuous.

=== Phase 2 — prove the 4 theorems

Proposed order (easiest first):

1. `js-symmetric` — algebraic, 2-3 lines
2. `entropy-nonnegative` — requires auxiliary `log₂-nonpos-on-01` lemma (postulated as FFI fact)
3. `kl-nonnegative` — requires Gibbs/log-sum lemma
4. `js-bounded` — hardest; may require importing from an Agda analysis library

=== Phase 3 — convert FFI postulates to trust-tagged axioms

Add `@trust(level=axiom, prover=ffi, since=...)` inline annotations above each
of the 5 float postulates so the innervation layer records their trust level.

== Recorded as VeriSimDB octads (once deployed)

Each postulate should produce a `proof-status` octad with:

- `trust_level`: `axiom` (for FFI) or `postulate` (for provable theorems)
- `axioms_used`: list of float primitives
- Temporal: `verified_at` = null for postulates, set for any that get proven
