feat: real proof gate + typell bridge (route δ opened for measurement) (#44)

## What

Kategoria's 13 Idris 2 modules were genuinely verified — but nothing
enforced it: `just test` was a TODO echo stub, no workflow ever ran
`idris2`, and the repo's own metadata (`STATE.a2ml`, `TOPOLOGY.md`,
README scorecard) misdescribed or understated the work. This PR makes
the real work visible and enforced, then opens route δ by registering
**typell** as its first measurement target.

## Changes

- **Proof gate**: `scripts/check-idris2-proofs.sh` — hard-fails when
`idris2` is absent (a gate that skips is not a gate), checks all 13
modules, rejects axiom smuggling
(`postulate`/`believe_me`/`assert_total`/`%hint` outside comments).
Verified 13/13 under Idris 2 **0.7.0** and **0.8.0**; negative-tested
without the prover (exit 1).
- **CI**: `.github/workflows/proof-gate.yml` — the first workflow that
compiles this repo's substance, on every push/PR.
- **Justfile**: `test`/`build` now run the gate.
- **Dependabot**: drop 5 phantom ecosystems (no cargo/mix/npm/hex/pip
manifests exist) that have been failing since 2026-07-14.
- **De-drift**: TOPOLOGY.md documents the real layout (the
`approach-1..5/` + `spec/` map never existed); ROADMAP route-α table
matches measured reality (L8 ✓ via dependent-pair encoding; L4 = Type
Classes; L10 wall stands); README Progress scorecard row α filled (9 ✓,
L10 ✗); STATE.a2ml replaced (was RSR-template residue describing the
*template repo*).
- **Quarantine**: `src/interface/ffi` is uninstantiated template
scaffold (`{{project}}` placeholders — cannot compile under any zig);
documented, excluded from gates. Follow-up decision: instantiate for
route δ's ABI or remove.
- **Route δ bridge**: `routes/delta-aggregate/TYPELL-BRIDGE.adoc` —
reconciles the **colliding L1–L10 hierarchies** (kategoria = language
features; typell = safety properties; only L9 aligns), gives an
evidence-backed enablement matrix against `typell-core`, and defines
what flows each way. Companion typell PR adds the conformance suite +
fixes typell's own (never-run, currently failing) Idris ABI proofs.

## Verification

- `just proof-check` → `PASS=13 FAIL=0` (run under both prover versions)
- Negative test: hiding `idris2` from PATH → exit 1 with FATAL message
- Not touched: secret-scanner/gitleaks workflows (owned by the parallel
security sweep)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Author: hyperpolymath

.github/dependabot.yml

@@ -1,10 +1,13 @@
 # SPDX-License-Identifier: MPL-2.0
-# Dependabot configuration for RSR-compliant repositories
-# Covers common ecosystems - remove unused ones for your project
+# Dependabot configuration for kategoria.
+#
+# This repo's code is Idris 2 (no package manifest Dependabot understands)
+# plus GitHub Actions workflows. Declaring ecosystems without manifests
+# (cargo/mix/npm/hex/pip from the RSR template) produced 5 standing
+# Dependabot failures on 2026-07-14 — only github-actions is real here.
 
 version: 2
 updates:
-  # GitHub Actions - always include
   - package-ecosystem: "github-actions"
     directory: "/"
     schedule:
@@ -13,39 +16,3 @@ updates:
       actions:
         patterns:
           - "*"
-
-  # Rust/Cargo
-  - package-ecosystem: "cargo"
-    directory: "/"
-    schedule:
-      interval: "weekly"
-    # `open-pull-requests-limit: 0` suppresses routine version-update PRs
-    # while leaving Dependabot SECURITY PRs flowing. The previous
-    # `ignore: "*" patch` rule also silenced security PRs under GitHub\'s
-    # current Dependabot behaviour. See rsr-template-repo commit 78b050e
-    # and 007-lang/audits/audit-dependabot-automation-gap-2026-04-17.md.
-    open-pull-requests-limit: 0
-
-  # Elixir/Mix
-  - package-ecosystem: "mix"
-    directory: "/"
-    schedule:
-      interval: "weekly"
-
-  # Node.js/npm
-  - package-ecosystem: "npm"
-    directory: "/"
-    schedule:
-      interval: "weekly"
-
-  # Python/pip
-  - package-ecosystem: "pip"
-    directory: "/"
-    schedule:
-      interval: "weekly"
-
-  # Nix flakes
-  - package-ecosystem: "nix"
-    directory: "/"
-    schedule:
-      interval: "weekly"

.github/workflows/proof-gate.yml

@@ -0,0 +1,31 @@
+# SPDX-License-Identifier: MPL-2.0
+# Proof Gate — type-checks the repo's real substance on every push and PR.
+#
+# This is the FIRST workflow in this repository that compiles the Idris 2
+# modules the project exists to produce. It hard-fails when the prover is
+# missing (scripts/check-idris2-proofs.sh refuses to skip).
+#
+# Verified locally under Idris 2 0.7.0 (system) and 0.8.0 (nixpkgs):
+# 13/13 modules PASS, axiom-smuggling scan clean.
+name: Proof Gate
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  idris2-proofs:
+    name: idris2 --check (13 modules)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - uses: cachix/install-nix-action@a49548c11d9846ad46ecc0115273879b045f001c # v31.10.7
+
+      - name: Run proof gate
+        run: nix shell nixpkgs#idris2 -c ./scripts/check-idris2-proofs.sh

.machine_readable/6a2/STATE.a2ml

@@ -1,64 +1,61 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# STATE.a2ml — Project state checkpoint (META-TEMPLATE)
+# STATE.a2ml — Project state checkpoint for kategoria.
 #
-# This is the STATE file for kategoria.
-# When consumed by a new project, replace {{PLACEHOLDER}} tokens
-# and customize sections below for the target project.
+# HISTORY NOTE: until 2026-07-21 this file was unedited RSR-template
+# residue describing the TEMPLATE repository ("95% complete, production,
+# maintenance"). Everything below is measured project state.
 
 [metadata]
 project = "kategoria"
-version = "0.2.0"
-last-updated = "2026-02-28"
+version = "0.1.0"
+last-updated = "2026-07-21"
 status = "active"  # active | paused | archived
 
 [project-context]
 name = "kategoria"
-purpose = "Canonical RSR-compliant repository template providing scaffolding for all hyperpolymath projects — including CI/CD, AI manifests, ABI/FFI standards, container ecosystem, and governance infrastructure."
-completion-percentage = 95
+purpose = "The Type Safety Challenge: five independent language-implementation routes (α Extend Idris 2, β Dyadic, γ Aspect, δ Aggregate, ε Clean Slate) exploring all 10 known levels of type safety. Named after Aristotle's Categories."
+completion-percentage = 25
 
 [position]
-phase = "maintenance"      # design | implementation | testing | maintenance | archived
-maturity = "production"    # experimental | alpha | beta | production | lts
+phase = "implementation"   # design | implementation | testing | maintenance | archived
+maturity = "alpha"         # experimental | alpha | beta | production | lts
+
+[verification]
+# Enforced by scripts/check-idris2-proofs.sh (Proof Gate workflow on push/PR).
+# The gate HARD-FAILS when idris2 is absent and rejects axiom smuggling
+# (postulate / believe_me / assert_total / %hint outside comments).
+proof-modules = 13
+proof-modules-passing = 13
+provers-verified = ["Idris 2 0.7.0", "Idris 2 0.8.0 (nixpkgs)"]
+last-verified = "2026-07-21"
 
 [route-to-mvp]
 milestones = [
-  { name = "Phase 0: Core scaffolding (justfile, CI/CD, .machine_readable)", completion = 100 },
-  { name = "Phase 1: ABI/FFI standard (Idris2/Zig templates)", completion = 100 },
-  { name = "Phase 1b: AI Gatekeeper Protocol (0-AI-MANIFEST.a2ml)", completion = 100 },
-  { name = "Phase 1c: TOPOLOGY.md standard and guide", completion = 100 },
-  { name = "Phase 1d: Maintenance gate (axes, checklist, approach)", completion = 100 },
-  { name = "Phase 1e: Trustfile / contractiles", completion = 100 },
-  { name = "Phase 2: Container ecosystem templates (stapeln)", completion = 100 },
-  { name = "Phase 3: Multi-forge sync hardening", completion = 0 },
-  { name = "Phase 4: Nix/Guix reproducible shells", completion = 50 },
+  { name = "Route α: L1-L7 native Idris 2, verified", completion = 100 },
+  { name = "Route α: L8 refinement (dependent-pair encoding), L9 sessions (Brady indexed monad)", completion = 100 },
+  { name = "Route α: L10 cubical — WALL, documented as impossible on this route", completion = 100 },
+  { name = "Proof gate: script + Justfile + CI (cannot silently pass)", completion = 100 },
+  { name = "Route δ: typell bridge (routes/delta-aggregate/TYPELL-BRIDGE.adoc)", completion = 40 },
+  { name = "Route δ: full aggregate (F*/LH + Scribble + Agda --cubical over one ABI)", completion = 0 },
+  { name = "Routes β, γ: not started", completion = 0 },
+  { name = "Route ε: research phase (Nuyts/Devriese 2023, Gratzer et al. 2024)", completion = 5 },
 ]
 
 [blockers-and-issues]
-# No active blockers
+issues = [
+  "src/interface/ffi is uninstantiated RSR template scaffold ({{project}} placeholders, does not compile under any zig) — quarantined in TOPOLOGY.md; instantiate or remove when a route needs a C ABI",
+  "13 stale remote branches, all unmerged by commit-graph (probable squash-merge artifacts) — prune needs per-branch content diff",
+]
 
 [critical-next-actions]
 actions = [
-  "Container templates complete — test with `just container-init`",
-  "Validate container templates across wolfi-base and static Chainguard images",
-  "Harden multi-forge sync for GitLab/Bitbucket mirroring edge cases",
-  "Expand Nix/Guix development shell templates",
+  "Land typell conformance suite (typell repo: crates/typell-core/tests/kategoria_conformance.rs)",
+  "Decide src/interface/ffi disposition (instantiate for route δ ABI vs remove)",
+  "Route δ next step: Agda --cubical bridge prototype for L10",
 ]
 
-[maintenance-status]
-last-run-utc = "never"
-last-report = "docs/reports/maintenance/latest.json"
-last-result = "unknown"  # unknown | pass | warn | fail
-open-warnings = 0
-open-failures = 0
-
 [ecosystem]
-part-of = ["RSR Framework", "stapeln ecosystem"]
-depends-on = ["stapeln", "selur-compose", "cerro-torre", "svalinn", "vordr", "k9-svc"]
-
-# ---------------------------------------------------------------------------
-# NOTE FOR CONSUMERS: When using this template to create a new repo, reset
-# the fields above to your project's values and replace all {{PLACEHOLDER}}
-# tokens. The milestones above describe the TEMPLATE's evolution, not yours.
-# ---------------------------------------------------------------------------
+part-of = ["hyperpolymath type-safety programme"]
+related = ["typell (aggregate-style verification kernel; bridge registered)", "panll (consumes typell)", "007", "typed-wasm", "nextgen-languages"]

.tool-versions

@@ -1,10 +1 @@
-# Uncomment and customize for your project
-# rust nightly
-# just 1.40.0
-# nickel 1.10.0
-# gleam 1.8.0
-# elixir 1.18.0
-# erlang 27.2
-# zig 0.14.0
-# idris2 0.7.0
-rust nightly
+idris2 0.7.0

Justfile

@@ -265,14 +265,8 @@ init:
 # ═══════════════════════════════════════════════════════════════════════════════
 
 # Build the project (debug mode)
-build *args:
-    @echo "Building {{project}} (debug)..."
-    # TODO: Replace with your build command
-    # Examples:
-    #   cargo build {{args}}                    # Rust
-    #   mix compile {{args}}                    # Elixir
-    #   zig build {{args}}                      # Zig
-    #   deno task build {{args}}                # Deno/ReScript
+build *args: proof-check
+    @echo "kategoria's build IS type-checking: proof-check ran above."
     @echo "Build complete"
 
 # Build in release mode with optimizations
@@ -309,15 +303,12 @@ clean-all: clean
 # ═══════════════════════════════════════════════════════════════════════════════
 
 # Run all tests
-test *args:
-    @echo "Running tests..."
-    # TODO: Replace with your test command
-    # Examples:
-    #   cargo test {{args}}
-    #   mix test {{args}}
-    #   zig build test {{args}}
-    #   deno test {{args}}
-    @echo "Tests passed!"
+test *args: proof-check
+
+# Type-check all 13 verified Idris 2 modules (the repo's real substance).
+# Hard-fails when idris2 is absent — a gate that skips is not a gate.
+proof-check:
+    ./scripts/check-idris2-proofs.sh
 
 # Run tests with verbose output
 test-verbose:

README.md

@@ -236,15 +236,26 @@ field reports.
 
 | Route       | L1  | L2  | L3  | L4  | L5  | L6  | L7  | L8  | L9  | L10 |
 |-------------|-----|-----|-----|-----|-----|-----|-----|-----|-----|-----|
-| α Extend    |     |     |     |     |     |     |     |     |     |     |
-| β Dyadic    |     |     |     |     |     |     |     |     |     |     |
-| γ Aspect    |     |     |     |     |     |     |     |     |     |     |
-| δ Aggregate |     |     |     |     |     |     |     |     |     |     |
-| ε Clean     |     |     |     |     |     |     |     |     |     |     |
+| α Extend    | ✓   | ✓   | ✓   | ✓   | ✓   | ✓   | ✓   | ✓   | ✓   | ✗   |
+| β Dyadic    | .   | .   | .   | .   | .   | .   | .   | .   | .   | .   |
+| γ Aspect    | .   | .   | .   | .   | .   | .   | .   | .   | .   | .   |
+| δ Aggregate | .   | .   | .   | .   | .   | .   | .   | .   | .   | .   |
+| ε Clean     | .   | .   | .   | .   | .   | .   | .   | .   | .   | .   |
 
 *(✓ = passing, ~ = partial, . = not started, ✗ = proven impossible on
 this route)*
 
+Route α's row is enforced by CI: `scripts/check-idris2-proofs.sh` type-checks
+all 13 modules (verified under Idris 2 0.7.0 and 0.8.0) and rejects axiom
+smuggling. L8 and L9 pass via encodings (dependent pairs; Brady's indexed
+monad); L10 is route α's documented wall — see
+`routes/alpha-extend/Level10_CubicalTypes.idr`.
+
+Route δ has a measurement bridge before it has an implementation: the
+[typell](https://github.com/hyperpolymath/typell) verification kernel is a
+live aggregate-style engine mapped level-by-level in
+[`routes/delta-aggregate/TYPELL-BRIDGE.adoc`](routes/delta-aggregate/TYPELL-BRIDGE.adoc).
+
 # Level 11 and Beyond
 
 > [!IMPORTANT]

ROADMAP.adoc

@@ -2,9 +2,13 @@
 = Kategoria Roadmap
 :author: Jonathan D.A. Jewell
 
-== Current Status (2026-03-29)
+== Current Status (2026-07-21)
 
-Route α (Extend Idris 2) is the most advanced route.
+Route α (Extend Idris 2) is the most advanced route. All 13 modules
+(10 levels + 3 demos) pass `idris2 --check` under Idris 2 0.7.0 AND 0.8.0
+with no postulates, believe_me, or %hint smuggling — enforced by
+`scripts/check-idris2-proofs.sh` (the Proof Gate workflow runs it on every
+push and PR).
 
 === Route α Progress
 
@@ -14,23 +18,31 @@ Route α (Extend Idris 2) is the most advanced route.
 
 | 1 | Basic Types | ✓ | `Level01_BasicTypes.idr`
 | 2 | ADTs | ✓ | `Level02_ADTs.idr`
-| 3 | Parametric Polymorphism | ✓ | Native (Idris 2)
-| 4 | Higher-Kinded Types | ✓ | Native (Idris 2)
-| 5 | GADTs | ✓ | Native (Idris 2)
+| 3 | Parametric Polymorphism | ✓ | `Level03_Polymorphism.idr`
+| 4 | Type Classes | ✓ | `Level04_TypeClasses.idr`
+| 5 | GADTs | ✓ | `Level05_GADTs.idr`
 | 6 | Dependent Types | ✓ | `Level06_DependentTypes.idr`
-| 7 | Linear Types | ✓ | Native (QTT)
-| 8 | Refinement Types | ~ | Elaborator sugar in progress
-| 9 | Session Types | ✓ | `Level09_SessionTypes.idr`
-| 10 | Cubical/Homotopy | ✗ | `Level10_CubicalTypes.idr` (wall documented)
+| 7 | Linear Types | ✓ | `Level07_LinearTypes.idr` (native QTT)
+| 8 | Refinement Types | ✓ | `Level08_Refinement.idr` (dependent-pair encoding, auto-search proofs)
+| 9 | Session Types | ✓ | `Level09_SessionTypes.idr` (Brady indexed-monad encoding)
+| 10 | Cubical/Homotopy | ✗ | `Level10_CubicalTypes.idr` (wall documented; type-checks as an honest engineering record, does not deliver univalence)
 |===
 
-*Route α score: 9/10 (8 native + 1 encoding, 1 impossible)*
+*Route α score: 9/10 (7 native + 2 encodings, 1 impossible)*
 
 === Other Routes
 
 - **Route β (Dyadic)**: Not started. Next priority for L10.
 - **Route γ (Aspect)**: Not started. L10 as aspect is risky (see cross-pollination #001).
-- **Route δ (Aggregate)**: Not started. Bridge to Agda --cubical is fastest path to L10.
+- **Route δ (Aggregate)**: Opened 2026-07-21 via the typell bridge —
+  link:routes/delta-aggregate/TYPELL-BRIDGE.adoc[TYPELL-BRIDGE.adoc] maps the
+  https://github.com/hyperpolymath/typell[typell] verification kernel
+  (a live aggregate-style engine: HM + dependent lengths + QTT/linear +
+  effects + sessions + refinement/SMT + dimensional, 225 kernel tests) onto
+  kategoria's levels. Typell is NOT the full route δ prescription
+  (Idris 2 + F*/Liquid Haskell + Scribble + Agda --cubical over one ABI),
+  but it is the first concrete aggregate implementation to measure against.
+  Bridge to Agda --cubical remains the fastest path to L10.
 - **Route ε (Clean Slate)**: Research phase. Reading Nuyts & Devriese (2023), Gratzer et al. (2024).
 
 == Milestones
@@ -39,8 +51,9 @@ Route α (Extend Idris 2) is the most advanced route.
 * [x] L1-L7: Native Idris 2 coverage verified
 * [x] L9: Session types via indexed monad encoding
 * [x] L10: Wall documented with best-effort encoding
-* [ ] L8: Refinement types via elaborator sugar
-* [ ] Shared test suite: all challenge programs automated
+* [x] L8: Refinement types via dependent-pair encoding (2026-06; `%auto_implicit_depth` for literal bounds)
+* [x] Route α programs automated: `just proof-check` + Proof Gate CI (2026-07-21)
+* [ ] Shared test suite generalized across routes (only α has code today)
 
 === v0.2.0 — Second Route Begins
 * [ ] Route δ: Bridge to Agda --cubical for L10