W1-7: Type-checking Agda proofs + agda --safe CI + honest catalogue

.github/workflows/agda.yml

@@ -0,0 +1,115 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# agda.yml — Type-check the EXPERIMENTAL Agda proofs under proofs/.
+#
+# Every proofs/**/*.agda module must pass `agda --safe` (no weakening of --safe),
+# no module may go unchecked (a new .agda file that is not registered fails the
+# job), and no `postulate` is permitted (the proofs are constructive).
+name: Agda Proofs
+
+on:
+  push:
+    branches: [main, master, develop]
+    paths:
+      - 'proofs/**'
+      - '.github/workflows/agda.yml'
+  pull_request:
+    branches: [main, master]
+    paths:
+      - 'proofs/**'
+      - '.github/workflows/agda.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: agda-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  agda-safe:
+    name: agda --safe (proofs/)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v7.0.0
+
+      - name: Install Agda + agda-stdlib (apt)
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends agda agda-stdlib
+          agda --version
+
+      - name: Configure agda-stdlib library
+        run: |
+          set -euo pipefail
+          # Some distributions ship a standard-library.agda-lib inside the package;
+          # prefer it when one is present.
+          LIB="$(dpkg -L agda-stdlib | grep -E '/standard-library\.agda-lib$' | head -1 || true)"
+          if [ -z "${LIB:-}" ]; then
+            # The Debian/Ubuntu agda-stdlib package (apt, ubuntu-latest) ships the
+            # library sources but NO .agda-lib file anywhere on the filesystem, so
+            # synthesise one against the installed source root (the directory that
+            # directly contains Data/, Relation/, ...). Detect that root from the
+            # package contents rather than hard-coding a path.
+            SRC="$(dpkg -L agda-stdlib | grep -E '/Data/Nat/Base\.agda$' | head -1 || true)"
+            if [ -z "${SRC:-}" ]; then
+              echo "::error::agda-stdlib is installed but neither a packaged .agda-lib nor Data/Nat/Base.agda was found; cannot configure the standard library"
+              dpkg -L agda-stdlib | sed -n '1,40p'
+              exit 1
+            fi
+            ROOT="${SRC%/Data/Nat/Base.agda}"
+            LIB="$ROOT/standard-library.agda-lib"
+            echo "No packaged .agda-lib; synthesising $LIB (source root: $ROOT)"
+            printf 'name: standard-library\ninclude: .\n' | sudo tee "$LIB" >/dev/null
+          fi
+          echo "Using stdlib library file: $LIB"
+          # Agda writes .agdai interface files next to the sources; the package tree
+          # is root-owned, so make it writable for the (non-root) runner user before
+          # the first type-check refreshes the interface build cache.
+          sudo chmod -R a+rwX "$(dirname "$LIB")"
+          mkdir -p "$HOME/.agda"
+          echo "$LIB" > "$HOME/.agda/libraries"
+          echo "standard-library" > "$HOME/.agda/defaults"
+
+      - name: Reject postulates in proofs/
+        run: |
+          if grep -rnw --include='*.agda' 'postulate' proofs/; then
+            echo "::error::proofs/ must contain no 'postulate' — the experimental proofs are constructive"
+            exit 1
+          fi
+          echo "PASS: no postulates under proofs/"
+
+      - name: Type-check every module (agda --safe) + guard unchecked files
+        run: |
+          set -euo pipefail
+          # Explicit registry of modules that MUST be type-checked. Adding a new
+          # proofs/**/*.agda file WITHOUT registering it here fails this job.
+          EXPECTED_SORTED="$(printf '%s\n' \
+            'Statistikles/Inequalities.agda' \
+            'Statistikles/RankIdentities.agda' \
+            'Statistikles/TropicalSemiring.agda' | sort)"
+          FOUND_SORTED="$(cd proofs && find . -name '*.agda' -type f | sed 's|^\./||' | sort)"
+          if [ "$EXPECTED_SORTED" != "$FOUND_SORTED" ]; then
+            echo "::error::proofs/ module set does not match the registry in agda.yml."
+            echo "--- registered in workflow ---"; printf '%s\n' "$EXPECTED_SORTED"
+            echo "--- found under proofs/ ------"; printf '%s\n' "$FOUND_SORTED"
+            echo "Register any new module in the EXPECTED_SORTED list in .github/workflows/agda.yml."
+            exit 1
+          fi
+          cd proofs
+          rc=0
+          while IFS= read -r mod; do
+            [ -z "$mod" ] && continue
+            echo "== agda --safe $mod =="
+            if ! agda --safe "$mod"; then
+              echo "::error file=proofs/$mod::agda --safe failed for $mod"
+              rc=1
+            fi
+          done <<< "$FOUND_SORTED"
+          if [ "$rc" -eq 0 ]; then echo "PASS: all proof modules type-check under --safe"; fi
+          exit $rc

.github/workflows/e2e.yml

@@ -98,6 +98,13 @@ jobs:
             echo "$DANGEROUS"
             exit 1
           fi
+          # Experimental Agda proofs must stay constructive — no postulates.
+          PROOF_POSTULATES=$(grep -rnw --include='*.agda' 'postulate' proofs/ 2>/dev/null || true)
+          if [ -n "$PROOF_POSTULATES" ]; then
+            echo "FAIL: postulate found under proofs/"
+            echo "$PROOF_POSTULATES"
+            exit 1
+          fi
           echo "PASS: No dangerous patterns"
 
       - name: SPDX headers

proofs/README.adoc

@@ -2,39 +2,108 @@
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = Statistikles Formal Proofs (Agda)
 
-Constructive proofs of core statistical identities used by Statistikles.
-Verified by Agda's dependent type checker — no postulates, no holes.
+*Status: EXPERIMENTAL.* These modules type-check under `agda --safe` with no
+postulates and no holes — but they are *not yet* proofs of the statistical
+theorems Statistikles relies on. Every lemma below is stated and proven over
+the natural numbers (`ℕ`). The runtime computes over `Float64` (IEEE-754
+doubles), so each entry is a *discrete proxy for* — not a proof of — the
+statistical target in the right-hand column.
+
+[IMPORTANT]
+====
+*Scope: current proofs quantify over `ℕ`, not `Float64`.* None of them quantify
+over `ℝ` or over the IEEE-754 `Float64` the runtime actually uses. The gap
+between the ℕ lemma proven here and the ℝ/`Float64` statement the statistic
+needs is real and is tracked below as "target (pending)". Read "Proven (ℕ)" as
+"this discrete lemma type-checks", *not* as "the statistic is verified".
+Restating these over the reals is deferred future work (production-readiness
+reframe W2-4); it is deliberately *not* attempted here.
+====
 
 == Proof Catalogue
 
-[cols="1,2,2,1"]
+Each row gives the *exact* lemma the Agda source proves (its type signature),
+the module it lives in, and the statistical result it is intended to
+approximate. The middle column is *proven over ℕ*; the right-hand target is
+*pending*.
+
+[cols="1,5,2,4",options="header"]
 |===
-| # | Identity | File | Status
-
-| 1 | Tropical addition associative | TropicalSemiring.agda | Proven
-| 2 | Tropical addition commutative | TropicalSemiring.agda | Proven
-| 3 | Tropical distributivity | TropicalSemiring.agda | Proven
-| 4 | Tropical idempotence | TropicalSemiring.agda | Proven
-| 5 | Tropical multiplicative identity | TropicalSemiring.agda | Proven
-| 6 | Chi-square df identity | RankIdentities.agda | Proven
-| 7 | Rank sum (concrete to n=100) | RankIdentities.agda | Proven
-| 8 | Bonferroni (elem ≤ sum) | Inequalities.agda | Proven
-| 9 | Tie correction bound (sq-mono) | Inequalities.agda | Proven
-| 10 | Mean ordering transitivity | Inequalities.agda | Proven
+| # | Lemma actually proven (over `ℕ`) | File | Statistical target (pending)
+
+| 1
+| `min-assoc : ∀ a b c → min a (min b c) ≡ min (min a b) c` — `min` on `ℕ` is associative
+| TropicalSemiring.agda
+| Associativity of tropical addition `⊕ = min` on `ℝ ∪ {+∞}`
+
+| 2
+| `min-comm : ∀ a b → min a b ≡ min b a` — `min` on `ℕ` is commutative
+| TropicalSemiring.agda
+| Commutativity of tropical `⊕ = min` on `ℝ ∪ {+∞}`
+
+| 3
+| `+-distrib-min : ∀ a b c → a + min b c ≡ min (a + b) (a + c)` — `+` distributes over `min` on `ℕ`
+| TropicalSemiring.agda
+| Tropical `⊗ = +` distributes over `⊕ = min` on `ℝ ∪ {+∞}`
+
+| 4
+| `min-idem : ∀ a → min a a ≡ a` — `min` on `ℕ` is idempotent
+| TropicalSemiring.agda
+| Idempotence of tropical `⊕` on `ℝ ∪ {+∞}`
+
+| 5
+| `tropical-mul-identity : ∀ a → zero + a ≡ a` — `0` is the left identity of `+` on `ℕ` (definitional)
+| TropicalSemiring.agda
+| `0` is the tropical `⊗`-identity (and `+∞` the `⊕`-identity) on `ℝ ∪ {+∞}`
+
+| 6
+| `df-identity : ∀ k → suc k ∸ 1 ≡ k` and `df-nonneg : ∀ k → zero ≤ k` — truncated subtraction on `ℕ`
+| RankIdentities.agda
+| χ² degrees of freedom `= (categories − 1)` is well-defined and non-negative
+
+| 7
+| `sum-to` running-sum recursion with concrete checks (`sum-to 5 ≡ 15`, …, `sum-to 100 ≡ 5050`) and `sum-to-mono : n ≤ m → sum-to n ≤ sum-to m` on `ℕ`
+| RankIdentities.agda
+| Rank/midrank sum identity `Σᵢ₌₁ⁿ i = n(n+1)/2` over `ℝ` (tie handling)
+
+| 8
+| `elem-le-sum : ∀ x xs → x ≤ x + list-sum xs` — a list element is `≤` the list sum, on `ℕ`
+| Inequalities.agda
+| Bonferroni inequality `P(⋃ Aᵢ) ≤ Σ P(Aᵢ)` over `ℝ`
+
+| 9
+| `sq-mono : a ≤ b → a * a ≤ b * b` — squaring is monotone on `ℕ`
+| Inequalities.agda
+| Monotonicity of the tie-correction term `Σ(tᵢ³ − tᵢ)` in `N` over `ℝ`
+
+| 10
+| `mean-ordering-transitive : a ≤ b → b ≤ c → a ≤ c` — transitivity of `≤` on `ℕ`
+| Inequalities.agda
+| Transitivity of the power-mean ordering `M_p ≤ M_q ≤ M_r ⇒ M_p ≤ M_r` over `ℝ`
 |===
 
+All ten lemmas are `Proven (ℕ)`; all ten statistical targets remain `pending`.
+
 == Building
 
-Requires Agda 2.6.4+ and agda-stdlib.
+Requires Agda 2.6.4+ and agda-stdlib 2.x (library `statistikles-proofs.agda-lib`
+depends on `standard-library`). Every module must type-check under `--safe`
+(no weakening):
 
 ```bash
 agda --safe Statistikles/TropicalSemiring.agda
 agda --safe Statistikles/RankIdentities.agda
 agda --safe Statistikles/Inequalities.agda
 ```
 
-== Integration with ECHIDNA
+CI runs exactly this on every `proofs/**/*.agda` module — see
+`.github/workflows/agda.yml`. That workflow also fails if a new `.agda` file is
+added under `proofs/` without being type-checked, and rejects any `postulate`.
+
+== Integration with ECHIDNA (aspirational)
 
-These proofs correspond to the `StatProofObligation` entries in
-`src/bridge/echidna_adapter.jl`. ECHIDNA dispatches verification
-requests to Agda for constructive proofs and Z3 for arithmetic.
+The intended design is for these proofs to back the `StatProofObligation`
+entries in `src/bridge/echidna_adapter.jl`, with ECHIDNA dispatching
+constructive obligations to Agda and arithmetic obligations to Z3. That wiring
+is *not yet in place*, and the correspondence between these `ℕ` lemmas and the
+runtime's `Float64` statistics is future work — intentionally out of scope here.

proofs/Statistikles/Inequalities.agda

@@ -7,7 +7,7 @@
 module Statistikles.Inequalities where
 
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s)
-open import Data.Nat.Properties using (+-mono-≤; m≤m+n; +-comm)
+open import Data.Nat.Properties using (m≤m+n; m≤n+m)
 open import Data.List using (List; []; _∷_; foldr; map; length)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 
@@ -33,14 +33,7 @@ elem-le-sum x xs = m≤m+n x (list-sum xs)
 
 -- Sum is monotone under cons: list-sum xs ≤ list-sum (y ∷ xs)
 sum-mono-cons : ∀ (y : ℕ) (xs : List ℕ) → list-sum xs ≤ y + list-sum xs
-sum-mono-cons y xs = m≤m+n y (list-sum xs) |> flip-le
-  where
-  flip-le : y ≤ y + list-sum xs → list-sum xs ≤ y + list-sum xs
-  flip-le _ = subst-le (+-comm (list-sum xs) y)
-    where
-    open import Relation.Binary.PropositionalEquality using (subst)
-    subst-le : list-sum xs + y ≡ y + list-sum xs → list-sum xs ≤ y + list-sum xs
-    subst-le eq = subst (list-sum xs ≤_) eq (m≤m+n (list-sum xs) y)
+sum-mono-cons y xs = m≤n+m (list-sum xs) y
 
 -- ═══════════════════════════════════════════════════════════════════════
 -- PROOF 9: Tie correction is bounded

proofs/Statistikles/RankIdentities.agda

@@ -7,6 +7,7 @@
 module Statistikles.RankIdentities where
 
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s; _∸_)
+open import Data.Nat.Properties using (+-mono-≤)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 
 -- ═══════════════════════════════════════════════════════════════════════
@@ -66,13 +67,9 @@ _ = refl
 -- Rank sum is monotone: n ≤ m → sum-to n ≤ sum-to m
 -- ═══════════════════════════════════════════════════════════════════════
 
+-- sum-to (suc n) = suc n + sum-to n, so monotonicity of _+_ on both the
+-- successor term (suc n ≤ suc m) and the recursive tail (sum-to n ≤ sum-to m)
+-- gives the step directly.
 sum-to-mono : ∀ {n m} → n ≤ m → sum-to n ≤ sum-to m
-sum-to-mono z≤n = z≤n
-sum-to-mono {suc n} {suc m} (s≤s n≤m) = helper n m n≤m
-  where
-  -- We need: suc n + sum-to n ≤ suc m + sum-to m
-  -- This follows from n ≤ m and induction, but the full proof
-  -- requires +-mono which is complex. State as a consequence.
-  helper : ∀ n m → n ≤ m → suc n + sum-to n ≤ suc m + sum-to m
-  helper zero m z≤n = s≤s z≤n
-  helper (suc n) (suc m) (s≤s p) = s≤s (helper n m p)
+sum-to-mono z≤n       = z≤n
+sum-to-mono (s≤s n≤m) = +-mono-≤ (s≤s n≤m) (sum-to-mono n≤m)