proof: make Phronesis.agda compile; integrate echo-types (#39)

* proof: make Phronesis.agda compile; integrate echo-types (verdict provenance)

Phronesis.agda now type-checks (exit 0) for the first time. Root fixes:
ctx-cons _,_ -> _,,_ (mixfix ambiguity vs Data.Product._,_); drop two illegal
using+renaming repeats; complete the unsound/incomplete _≟ᵗ_ into a sound total
decidable type-equality (mutual _≟ᵗ_/_≟ᶠ_); fix _<ᵛ_ precedence+inference (Bool!=<ℤ).
PhronesisEcho.agda: an ethical verdict's provenance IS `Echo verdict v` —
verdict-forgets-provenance is the auditable-ethics headline. Machine-checked
vs real echo-types; adds phronesis-formal.agda-lib (depend: echo-types).

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

* fix(ci): codeql language matrix javascript-typescript -> actions; rm stale rot

CodeQL analyze hard-failed 'no source files': phronesis is Elixir/Erlang (BEAM),
not a CodeQL-supported language. Switch the matrix to `actions` (scans workflow
YAML — always present), restoring real SAST coverage (Hypatia SAST finding).
Also delete stale root artifacts flagged by Hypatia root_hygiene:
ECOSYSTEM.scm.bak, META.scm.bak, SPEC.core.scm.orig.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

---------

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

Author: hyperpolymath

.github/workflows/codeql.yml

@@ -28,7 +28,11 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - language: javascript-typescript
+          # Phronesis is Elixir/Erlang (BEAM) — not a CodeQL-supported source
+          # language, so `javascript-typescript` made `analyze` exit
+          # "no source files" on every run. `actions` scans the workflow YAML
+          # (always present), giving real SAST coverage. (Hypatia: SAST check.)
+          - language: actions
             build-mode: none
     steps:
       - name: Checkout