Merge branch 'main' into claude/dreamy-hypatia-O8XHo

Author: hyperpolymath

.github/ISSUE_TEMPLATE/bug_report.md

@@ -0,0 +1,38 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**To Reproduce**
+Steps to reproduce the behavior:
+1. Go to '...'
+2. Click on '....'
+3. Scroll down to '....'
+4. See error
+
+**Expected behavior**
+A clear and concise description of what you expected to happen.
+
+**Screenshots**
+If applicable, add screenshots to help explain your problem.
+
+**Desktop (please complete the following information):**
+ - OS: [e.g. iOS]
+ - Browser [e.g. chrome, safari]
+ - Version [e.g. 22]
+
+**Smartphone (please complete the following information):**
+ - Device: [e.g. iPhone6]
+ - OS: [e.g. iOS8.1]
+ - Browser [e.g. stock browser, safari]
+ - Version [e.g. 22]
+
+**Additional context**
+Add any other context about the problem here.

.github/ISSUE_TEMPLATE/custom.md

@@ -0,0 +1,10 @@
+---
+name: Custom issue template
+about: Describe this issue template's purpose here.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+

.github/ISSUE_TEMPLATE/feature_request.md

@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.

.github/workflows/agda.yml

@@ -33,7 +33,7 @@ jobs:
     timeout-minutes: 30
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10  # v6.0.3
 
       # Fast static gate (no Agda): enforce the EchoKernel funext-free
       # certificate and that every Echo*.agda is classified in
@@ -119,7 +119,7 @@ jobs:
       # source change or absolute-zero bump; restore-keys give a warm
       # partial cache even when it does.
       - name: Cache Agda interface files
-        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
         with:
           path: |
             ~/agda-stdlib/**/*.agdai
@@ -157,7 +157,7 @@ jobs:
     timeout-minutes: 30
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10  # v6.0.3
 
       - name: Install Agda
         run: |

.github/workflows/codeql.yml

@@ -42,15 +42,15 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
 
       - name: Initialize CodeQL
-        uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3
+        uses: github/codeql-action/init@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3
         with:
           languages: ${{ matrix.language }}
           build-mode: ${{ matrix.build-mode }}
 
       - name: Perform CodeQL Analysis
-        uses: github/codeql-action/analyze@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3
+        uses: github/codeql-action/analyze@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3
         with:
           category: "/language:${{ matrix.language }}"

.github/workflows/hypatia-scan.yml

@@ -49,7 +49,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           fetch-depth: 0  # Full history for better pattern analysis
 
@@ -108,7 +108,7 @@ jobs:
           echo "- Medium: $MEDIUM" >> $GITHUB_STEP_SUMMARY
 
       - name: Upload findings artifact
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         with:
           name: hypatia-findings
           path: hypatia-findings.json
@@ -244,7 +244,7 @@ jobs:
           always() &&
           (github.event_name != 'pull_request' ||
            github.event.pull_request.head.repo.fork != true)
-        uses: github/codeql-action/upload-sarif@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        uses: github/codeql-action/upload-sarif@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3.28.1
         with:
           sarif_file: hypatia.sarif
           # Distinct category so Hypatia results coexist with CodeQL's
@@ -384,7 +384,7 @@ jobs:
         # the pull-requests: write permission above: a token/API hiccup or
         # a fork PR (read-only token) skips the comment, not the check.
         continue-on-error: true
-        uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v7
+        uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v7
         with:
           script: |
             const fs = require('fs');

docs/bridge-status.md

@@ -47,3 +47,9 @@ This document strictly tracks the status of experimental extensions and bridges
 - **Dependencies:** None in this repo. Adjacent (downstream) only: Valence Shell (`hyperpolymath/valence-shell` — shell state transitions, undo/redo, checkpoints, diff/replay); Ochránce (`hyperpolymath/ochrance` — A2ML manifests, Merkle state commitments, repair/attestation surfaces).
 - **Blockers:** No shared schema and no mechanised cross-repo theorem exist. The relationship is citation-level only: Echo Types' structured-loss vocabulary (recoverable / constrained / residue-bearing / observationally equivalent / genuinely lost) is a *candidate* classifier for shell state transitions, and Ochránce may supply concrete receipt evidence. This is downstream application evidence, not a new foundation. Echo Types makes **no** claim about Valence Shell or Ochránce implementation correctness, and **no** claim about POSIX, Rust, the Lean→Rust correspondence, secure deletion, GDPR, cryptographic integrity, or attestation. Companion note: `docs/echo-types/explorations/accountable-shell/README.adoc`. Nothing for this bridge is imported into `proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, or `proofs/agda/EchoCanonicalIdentitySuite.agda`.
 - **Core Affect:** NO
+
+## 8. Eclexia consumer (thermodynamic resource bridge)
+- **Status:** LANDED (downstream consumer-side, in `hyperpolymath/eclexia` — PR eclexia#32). No artefact in *this* repo.
+- **Dependencies:** None in this repo. Adjacent (downstream) only: Eclexia (`hyperpolymath/eclexia` — the resource-typed "economics-as-code" language).
+- **Blockers:** None outstanding on the consumer side; this is application evidence, not a new foundation here. Eclexia integrates Echo as a first-class `Echo[A, B]` type former and, separately in its *own* Coq metatheory, mirrors the **discrete** thermodynamic shadow of this repo's `EchoThermodynamics` (`formal/coq/src/EchoThermo.v`: `bennett_reversible_is_free`, `free_iff_reversible`, `irreversible_costs_at_least_one_bit`, `erasure_monotone` — axiom-free, `Print Assumptions` clean), and exposes it at the language level as `landauer_cost(states, T) : Resource[Energy]` — pricing the erasure of a collapsed fibre (`k_B·T·ln N`; reversible retention is free). Echo Types makes **no** claim about Eclexia's implementation correctness; the real-valued `k T ln 2` scaling and the language runtime live entirely in that repo. The infinite-carrier collapse functional here remains negatively closed (`collapse-cost-impossible`, see §2) — eclexia consumes only the finite/discrete shadow. Nothing for this bridge is imported into `proofs/agda/All.agda` or `proofs/agda/Smoke.agda`.
+- **Core Affect:** NO