Skip to content

Commit c238e08

Browse files
hyperpolymathhyperpolymath
committed
docs: add theorem index, bridge status, and governance docs
This commit adds documents to improve proof auditability (theorem-index, bridge-status), enforce research boundaries (governance, research-boundaries), and establish verification procedures (build.md, check-no-unsafe.sh, verify.sh).
1 parent 97d8b82 commit c238e08

10 files changed

Lines changed: 168 additions & 0 deletions

File tree

‎docs/bridge-status.md‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
# Bridge Status
2+
3+
This document strictly tracks the status of experimental extensions and bridges between the minimal core of Echo Types and other domains.
4+
5+
**Note:** Bridge materials are speculative and exploratory. They do *not* affect the core identity or foundational theorems of the repository.
6+
7+
## 1. CNO Bridge (Absolute Zero)
8+
- **Status:** PARTIAL
9+
- **Dependencies:** Absolute Zero Framework
10+
- **Blockers:** End-to-end integration across repositories is not yet mechanically verified here.
11+
- **Core Affect:** NO
12+
13+
## 2. Thermodynamics
14+
- **Status:** EXPLORATORY
15+
- **Dependencies:** None
16+
- **Blockers:** The quantitative collapse functional on infinite carriers is negatively closed (`collapse-cost-impossible`).
17+
- **Core Affect:** NO
18+
19+
## 3. Tropical Semantics
20+
- **Status:** PARTIAL
21+
- **Dependencies:** None
22+
- **Blockers:** Witness residues under tropical collapse are established, but broader ecosystem mapping remains incomplete.
23+
- **Core Affect:** NO
24+
25+
## 4. Buchholz / Veblen Ordinals
26+
- **Status:** BLOCKED
27+
- **Dependencies:** Standard Agda
28+
- **Blockers:** Well-foundedness of shared-binder cases is blocked by the failure of the self-lift.
29+
- **Core Affect:** NO
30+
31+
## 5. JanusKey / Categorical
32+
- **Status:** EXPLORATORY
33+
- **Dependencies:** Categorical foundations
34+
- **Blockers:** Higher-level abstractions (monads, adjunctions) are still evolving; core functors are stable.
35+
- **Core Affect:** NO

‎docs/build.md‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
# Build Instructions
2+
3+
This repository contains mechanically verified proofs written in Agda.
4+
5+
## Prerequisites
6+
- Agda (with the standard library)
7+
- `just` (command runner)
8+
9+
## Verifying the Proofs
10+
11+
To run the complete verification suite, including safety checks and build steps:
12+
13+
```bash
14+
sh scripts/verify.sh
15+
```
16+
17+
To build the Agda proofs via `just`:
18+
19+
```bash
20+
just build-all
21+
```
22+
23+
To run the full suite via `just`:
24+
25+
```bash
26+
just test-all
27+
```

‎docs/governance.md‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
# Governance & Research Discipline
2+
3+
This repository operates under strict stabilisation and proof-preservation rules. It is treated as a sensitive proof artifact.
4+
5+
## Core vs. Bridge
6+
- **Core:** The minimal, mechanically verified theory of echo types (`proofs/agda/Echo/Core.agda`, `Characteristic.agda`, `Residue.agda`). This is the unshakeable foundation.
7+
- **Bridge:** Speculative extensions, cross-domain mappings, and integrations. Bridge materials are strictly labeled (e.g., PARTIAL, EXPLORATORY, BLOCKED) and reside in `proofs/agda/Echo/Bridges/` and `docs/bridges/`. They do *not* affect the core identity.
8+
9+
## Retractions
10+
- A claim is **RETRACTED** when fundamental type-theoretic or mathematical obstacles are encountered (e.g., Graded Comonad framing, Universal Property without funext).
11+
- Retracted claims are moved to `docs/retracted/`. They must not be revived without explicit new, mechanically verified proofs that overcome the documented blockers.
12+
13+
## Burden of Proof and Hidden Assumptions
14+
- Every substantive theorem must be mechanically checked in Agda.
15+
- **Prohibited:** Unsafe postulates, `TERMINATING` pragmas, `NON_TERMINATING` pragmas, `--allow-unsolved-metas`, and hidden assumptions.
16+
- If a proof cannot be completed, it must be left as a typed hole, annotated as a `TODO`, and explicitly labeled as `BLOCKED`.
17+
- Conjectures must be explicitly labeled as `CONJECTURE`.
18+
19+
## Modifications
20+
- Do not perform global namespace rewrites or aggressive file moves.
21+
- Favor small, proof-preserving commits.
22+
- Documentation must prioritize precision, restraint, and falsifiability over hype.

‎docs/research-boundaries.md‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# Research Boundaries
2+
3+
The goal of this project is to maintain a minimal, defensible core for Echo Types.
4+
5+
## What is In-Scope
6+
- **Proof-preserving cleanup:** Refactoring that maintains exact semantics and improves readability.
7+
- **Documentation precision:** Clarifying exact proof obligations, adding theorem indexes, and noting limitations.
8+
- **Compatibility hardening:** Using wrappers to ensure stable imports for dependent projects.
9+
- **Auditing:** Verification scripts that reject unsafe assumptions or pragmas.
10+
- **Minimal Canonical Examples:** Small, self-contained illustrations of structured loss (e.g., lossy boolean classification, provenance).
11+
12+
## What is Strictly Out-of-Scope
13+
- **Abstraction expansion:** Inventing new mathematical terminology or introducing large categorical frameworks unless strictly required by a specific, mechanically verified theorem.
14+
- **Theory growth:** Attempting to "complete" the theory beyond the established minimal core.
15+
- **Revisiting Retractions:** Revisiting graded-comonad framing, universal property framing, or thermodynamics without substantial new mechanical breakthroughs.
16+
- **Unsafe assumptions:** Introducing `postulate`, `TERMINATING`, or `--allow-unsolved-metas` to force a proof to pass.
17+
- **Overclaiming:** Using hype-driven terminology like "revolutionary" or "universal" in place of "mechanically checked" or "candidate."

‎docs/theorem-index.md‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
# Theorem Index
2+
3+
This document maps foundational theorems and characteristic results to their exact locations in the `proofs/agda/` tree.
4+
5+
## Foundational Core
6+
7+
| Theorem | Status | Module Path | Meaning |
8+
|---------|--------|-------------|---------|
9+
| `echo-intro` | PROVED | `Echo/Core.agda` | Introduction of an echo from the base point. |
10+
| `map-over` | PROVED | `Echo/Core.agda` | Action on fibers for morphisms over a fixed base. |
11+
| `map-over-comp` | PROVED | `Echo/Core.agda` | Composition law for fiber morphisms. |
12+
| `map-over-id` | PROVED | `Echo/Core.agda` | Identity law for fiber morphisms. |
13+
14+
## Characteristic Results
15+
16+
| Theorem | Status | Module Path | Meaning |
17+
|---------|--------|-------------|---------|
18+
| `collapse-non-injective` | PROVED | `Echo/Characteristic.agda` | Explicit witness of irreversible collapse. |
19+
| `no-section-collapse` | PROVED | `Echo/Characteristic.agda` | Impossibility of inverting the collapse map. |
20+
| `no-section-visible` | PROVED | `Echo/Characteristic.agda` | Impossibility of full reconstruction from visible output alone. |
21+
| `echo-true≢echo-false` | PROVED | `Echo/Characteristic.agda` | Distinct echoes exist over the same visible output. |
22+
| `visible-constraint` | PROVED | `Echo/Characteristic.agda` | Projection-style loss retains a provable constraint on the source. |
23+
| `no-section-collapse-to-residue` | PROVED | `Echo/Residue.agda` | Weakening an echo to a residue discards irrecoverable information. |
24+
25+
*Note: For experimental bridges or retracted claims, refer to the [Proof Obligation Ledger](proof-obligations.md) and [Bridge Status](bridge-status.md).*

‎proofs/agda/Echo.agda‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
{-# OPTIONS --safe --without-K #-}
22

3+
-- Compatibility Wrapper
4+
-- This module exists solely for import stability.
5+
-- It is a transitional surface to prevent breaking downstream dependencies.
6+
37
module Echo where
48

59
open import Echo.Core public

‎proofs/agda/EchoCharacteristic.agda‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
{-# OPTIONS --safe --without-K #-}
22

3+
-- Compatibility Wrapper
4+
-- This module exists solely for import stability.
5+
-- It is a transitional surface to prevent breaking downstream dependencies.
6+
37
module EchoCharacteristic where
48

59
open import Echo.Characteristic public

‎proofs/agda/EchoResidue.agda‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
{-# OPTIONS --safe --without-K #-}
22

3+
-- Compatibility Wrapper
4+
-- This module exists solely for import stability.
5+
-- It is a transitional surface to prevent breaking downstream dependencies.
6+
37
module EchoResidue where
48

59
open import Echo.Residue public

‎scripts/check-no-unsafe.sh‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#!/bin/sh
2+
3+
echo "Checking for unsafe constructs in proofs/agda..."
4+
5+
# Search for postulate, TERMINATING, NON_TERMINATING, allow-unsolved-metas, ignoring lines containing -- that explain the lack of postulates.
6+
UNSAFE=$(grep -rnE '^\s*postulate\b|{-# TERMINATING #-}|{-# NON_TERMINATING #-}|{-# OPTIONS.*--allow-unsolved-metas' proofs/agda)
7+
8+
if [ -n "$UNSAFE" ]; then
9+
echo "❌ Unsafe constructs found:"
10+
echo "$UNSAFE"
11+
exit 1
12+
fi
13+
14+
echo "✅ No unsafe constructs found."
15+
exit 0

‎scripts/verify.sh‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#!/bin/sh
2+
set -e
3+
4+
echo "Running verifications..."
5+
6+
echo "1. Checking no unsafe constructs..."
7+
sh scripts/check-no-unsafe.sh
8+
9+
echo "2. Building All.agda..."
10+
agda -i proofs/agda proofs/agda/All.agda
11+
12+
echo "3. Running just verify..."
13+
just verify
14+
15+
echo "✅ All verifications passed."

0 commit comments

Comments
 (0)