Skip to content

Commit 99864b5

Browse files
hyperpolymathhyperpolymath
committed
refactor: extract and isolate minimal defensible core
This commit reorganises the repository around a minimal core while preserving all compiling proofs. Bridge material and retracted claims have been explicitly isolated into docs/bridges, docs/retracted, and proofs/agda/Echo/Bridges.
1 parent b67c9ac commit 99864b5

76 files changed

Lines changed: 398 additions & 281 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎proofs/agda/All.agda‎

Lines changed: 51 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -2,75 +2,75 @@
22

33
module All where
44

5-
open import Echo
6-
open import AntiEcho
5+
open import Echo.Core
6+
open import Echo.Bridges.AntiEcho
77
open import EchoKernel
8-
open import EchoCharacteristic
9-
open import EchoResidue
10-
open import EchoExampleAbsInt
11-
open import EchoExampleParser
12-
open import EchoExampleProvenance
13-
open import EchoExamples
8+
open import Echo.Characteristic
9+
open import Echo.Residue
10+
open import Echo.Examples.EchoExampleAbsInt
11+
open import Echo.Examples.EchoExampleParser
12+
open import Echo.Examples.EchoExampleProvenance
13+
open import Echo.Examples.EchoExamples
1414

15-
open import EchoChoreo
16-
open import EchoEpistemic
15+
open import Echo.Bridges.EchoChoreo
16+
open import Echo.Bridges.EchoEpistemic
1717
open import EchoLinear
18-
open import EchoGraded
19-
open import EchoTropical
20-
open import AntiEchoTropical
21-
open import AntiEchoTropicalGeneric
22-
open import EchoIntegration
23-
open import EchoCNOBridge
18+
open import Echo.Bridges.EchoGraded
19+
open import Echo.Bridges.EchoTropical
20+
open import Echo.Bridges.AntiEchoTropical
21+
open import Echo.Bridges.AntiEchoTropicalGeneric
22+
open import Echo.Bridges.EchoIntegration
23+
open import Echo.Bridges.EchoCNOBridge
2424

25-
open import EchoApprox
26-
open import EchoApproxInstance
27-
open import EchoCost
28-
open import EchoCostInstance
29-
open import EchoIndexed
30-
open import EchoDecidable
31-
open import EchoSearch
32-
open import EchoSearchInstance
33-
open import EchoAccess
34-
open import EchoFiberCount
35-
open import EchoEpistemicResidue
36-
open import EchoRelational
37-
open import EchoCategorical
38-
open import EchoScope
39-
open import EchoOrdinal
40-
open import EchoJanusBridge
41-
open import Dyadic
42-
open import DyadicEchoBridge
43-
open import EchoThermodynamics
44-
open import EchoThermodynamicsFinite
45-
open import EchoThermodynamicsArbitrary
46-
open import EchoThermoCollapseImpossible
47-
open import EchoStabilityTests
25+
open import Echo.Bridges.EchoApprox
26+
open import Echo.Bridges.EchoApproxInstance
27+
open import Echo.Bridges.EchoCost
28+
open import Echo.Bridges.EchoCostInstance
29+
open import Echo.Bridges.EchoIndexed
30+
open import Echo.Bridges.EchoDecidable
31+
open import Echo.Bridges.EchoSearch
32+
open import Echo.Bridges.EchoSearchInstance
33+
open import Echo.Bridges.EchoAccess
34+
open import Echo.Bridges.EchoFiberCount
35+
open import Echo.Bridges.EchoEpistemicResidue
36+
open import Echo.Bridges.EchoRelational
37+
open import Echo.Bridges.EchoCategorical
38+
open import Echo.Bridges.EchoScope
39+
open import Echo.Bridges.EchoOrdinal
40+
open import Echo.Bridges.EchoJanusBridge
41+
open import Echo.Bridges.Dyadic
42+
open import Echo.Bridges.DyadicEchoBridge
43+
open import Echo.Bridges.EchoThermodynamics
44+
open import Echo.Bridges.EchoThermodynamicsFinite
45+
open import Echo.Bridges.EchoThermodynamicsArbitrary
46+
open import Echo.Bridges.EchoThermoCollapseImpossible
47+
open import Echo.Bridges.EchoStabilityTests
4848
open import VecRotation
4949

5050
-- Establishment-plan pillars (docs/echo-types/establishment-plan.adoc).
5151
-- A is a real bridge; B–D are doc-only scaffolds (no declarations,
5252
-- typecheck under --safe --without-K, tracked here per policy).
53-
open import EchoFiberBridge -- Pillar A (landed)
54-
open import EchoPullback -- Pillar B (scaffold)
55-
open import EchoGradedComonad -- Pillar B (scaffold)
56-
open import EchoSeparating -- Pillar C (scaffold)
57-
open import EchoRelModel -- Pillar D (scaffold)
53+
open import Echo.Bridges.EchoFiberBridge -- Pillar A (landed)
54+
open import Echo.Bridges.EchoPullback -- Pillar B (scaffold)
55+
open import Echo.Bridges.EchoGradedComonad -- Pillar B (scaffold)
56+
open import Echo.Bridges.EchoSeparating -- Pillar C (scaffold)
57+
open import Echo.Bridges.EchoRelModel -- Pillar D (scaffold)
5858

5959
-- Pillar F earn-back (docs/echo-types/earn-back-plan.adoc). Wired in
6060
-- on the gate passing (Sequencing pt 4); see docs/retractions.adoc
6161
-- follow-up F-2026-05-18a.
62-
open import EchoPullbackUnivF4 -- Gate F4 PASSED (funext-qualified UP)
63-
open import EchoStepNDModelF2 -- Gate F2 PASSED (StepND second model)
64-
open import EchoGradedComonadF1 -- Gate F1 PASSED (graded comonad on iterated-residue)
65-
open import EchoGradedComonadInterface -- Gate F3 abstract record
66-
open import EchoGradedComonadInstance1 -- Gate F3 instance 1 (F1 at (ℕ, +, 0))
67-
open import EchoGradedComonadInstance2 -- Gate F3 PASSED — instance 2 at (List Tag, ++, [])
62+
open import Echo.Bridges.EchoPullbackUnivF4 -- Gate F4 PASSED (funext-qualified UP)
63+
open import Echo.Bridges.EchoStepNDModelF2 -- Gate F2 PASSED (StepND second model)
64+
open import Echo.Bridges.EchoGradedComonadF1 -- Gate F1 PASSED (graded comonad on iterated-residue)
65+
open import Echo.Bridges.EchoGradedComonadInterface -- Gate F3 abstract record
66+
open import Echo.Bridges.EchoGradedComonadInstance1 -- Gate F3 instance 1 (F1 at (ℕ, +, 0))
67+
open import Echo.Bridges.EchoGradedComonadInstance2 -- Gate F3 PASSED — instance 2 at (List Tag, ++, [])
6868

6969
-- Foundation P1: external-fibre triangulation. Echo agrees with the
7070
-- standard library's OWN independently-authored notions
7171
-- (Function.Definitions / Function.Bundles), removing the
7272
-- same-module self-reference flagged by R-2026-05-18 finding 5.
73-
open import EchoFiberTriangulation
73+
open import Echo.Bridges.EchoFiberTriangulation
7474

7575
open import Ordinal.Base
7676
open import Ordinal.Closure

proofs/agda/AntiEcho.agda renamed to proofs/agda/Echo/Bridges/AntiEcho.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525
-- form) and `AntiEchoTropicalGeneric.agda` (generic-codomain lift
2626
-- over an abstract `OrderedCodomain` interface).
2727

28-
module AntiEcho where
28+
module Echo.Bridges.AntiEcho where
2929

3030
open import Level using (Level; _⊔_)
3131
open import Data.Empty using (⊥)
@@ -35,7 +35,7 @@ open import Function.Base using (_∘_)
3535
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
3636
open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
3737

38-
open import Echo using (Echo)
38+
open import Echo.Core using (Echo)
3939

4040
----------------------------------------------------------------------
4141
-- antiecho-def — the carrier.

proofs/agda/AntiEchoTropical.agda renamed to proofs/agda/Echo/Bridges/AntiEchoTropical.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -38,17 +38,17 @@
3838
-- `OrderedCodomain` interface (carrier `B`, `_≤_`, `_<_`, `≤⇒¬<`,
3939
-- `¬<⇒≤`).
4040

41-
module AntiEchoTropical where
41+
module Echo.Bridges.AntiEchoTropical where
4242

4343
open import Data.Empty using (⊥; ⊥-elim)
4444
open import Data.Nat.Base using (ℕ; zero; suc; _≤_; _<_; z≤n; s≤s)
4545
open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂)
4646
open import Function.Bundles using (_↔_; mk↔ₛ′)
4747
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
4848

49-
open import Echo using (Echo)
50-
open import AntiEcho using (AntiEcho)
51-
open import EchoTropical using (Candidate; score; IsArgmin; TropEcho)
49+
open import Echo.Core using (Echo)
50+
open import Echo.Bridges.AntiEcho using (AntiEcho)
51+
open import Echo.Bridges.EchoTropical using (Candidate; score; IsArgmin; TropEcho)
5252

5353
----------------------------------------------------------------------
5454
-- The headline decomposition: TropEcho ↔ Echo × Π-bound.

proofs/agda/AntiEchoTropicalGeneric.agda renamed to proofs/agda/Echo/Bridges/AntiEchoTropicalGeneric.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,14 @@
3030
-- "a generic-codomain version is deferred (would need a `≤`-bearing
3131
-- ordered codomain)" — that obligation is now landed here.
3232

33-
module AntiEchoTropicalGeneric where
33+
module Echo.Bridges.AntiEchoTropicalGeneric where
3434

3535
open import Data.Empty using (⊥)
3636
open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂)
3737
open import Function.Bundles using (_↔_; mk↔ₛ′)
3838
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
3939

40-
open import Echo using (Echo)
40+
open import Echo.Core using (Echo)
4141

4242
----------------------------------------------------------------------
4343
-- Ordered codomain interface.

proofs/agda/Dyadic.agda renamed to proofs/agda/Echo/Bridges/Dyadic.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
-- Formalization of two-party protocol types with dual checking.
66
-- Simplified to focus on the core dyadic session type structure.
77

8-
module Dyadic where
8+
module Echo.Bridges.Dyadic where
99

1010
open import Data.Unit.Base using (⊤; tt)
1111
open import Data.Empty using (⊥)

proofs/agda/DyadicEchoBridge.agda renamed to proofs/agda/Echo/Bridges/DyadicEchoBridge.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@
55
-- Integration of dyadic session types with echo types for provenance tracking.
66
-- Shows how echo types can retain protocol provenance in dyadic communications.
77

8-
module DyadicEchoBridge where
8+
module Echo.Bridges.DyadicEchoBridge where
99

10-
open import Dyadic
11-
open import Echo
10+
open import Echo.Bridges.Dyadic
11+
open import Echo.Core
1212

1313
open import Data.Unit.Base using (⊤; tt)
1414
open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂)

proofs/agda/EchoAccess.agda renamed to proofs/agda/Echo/Bridges/EchoAccess.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -74,16 +74,16 @@
7474
-- (⊎-shape honest+placeholder) considered as a future affordance
7575
-- if a real use-case for existential extraction emerges.
7676

77-
module EchoAccess where
77+
module Echo.Bridges.EchoAccess where
7878

7979
open import Level using (Level; _⊔_)
8080
open import Data.Unit.Base using (⊤; tt)
8181
open import Data.Product.Base using (Σ; _,_)
8282
open import Relation.Nullary.Decidable.Core using (yes)
8383
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
8484

85-
open import Echo using (Echo)
86-
open import EchoDecidable using (EchoDec)
85+
open import Echo.Core using (Echo)
86+
open import Echo.Bridges.EchoDecidable using (EchoDec)
8787

8888
----------------------------------------------------------------------
8989
-- 1. The access enum

proofs/agda/EchoApprox.agda renamed to proofs/agda/Echo/Bridges/EchoApprox.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -87,14 +87,14 @@
8787
-- `echo-approx-comp-retract-from-to` captures the strongest
8888
-- A-component statement available without that extra hypothesis.
8989

90-
module EchoApprox where
90+
module Echo.Bridges.EchoApprox where
9191

9292
open import Level using (Level; _⊔_; suc)
9393
open import Function.Base using (_∘_; id)
9494
open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂)
9595
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst)
9696

97-
open import Echo using (Echo)
97+
open import Echo.Core using (Echo)
9898

9999
----------------------------------------------------------------------
100100
-- Tolerance carrier and pseudo-metric structure

proofs/agda/EchoApproxInstance.agda renamed to proofs/agda/Echo/Bridges/EchoApproxInstance.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,13 +37,13 @@
3737
-- the purposes of `Smoke.agda` pinning. When a genuine metric instance
3838
-- lands in the repo, the per-lemma pins below can be re-pointed at it.
3939

40-
module EchoApproxInstance where
40+
module Echo.Bridges.EchoApproxInstance where
4141

4242
open import Level using (Level)
4343
open import Data.Unit.Base using (⊤; tt)
4444
open import Relation.Binary.PropositionalEquality using (refl)
4545

46-
open import EchoApprox using (Tolerance; PseudoMetric; BalancedTolerance; module Approx)
46+
open import Echo.Bridges.EchoApprox using (Tolerance; PseudoMetric; BalancedTolerance; module Approx)
4747

4848
----------------------------------------------------------------------
4949
-- The trivial tolerance carrier

proofs/agda/EchoCNOBridge.agda renamed to proofs/agda/Echo/Bridges/EchoCNOBridge.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,9 @@
2525
-- A patch addressing both is filed alongside this commit at
2626
-- `docs/echo-types/issue-21-absolute-zero.patch`.
2727

28-
module EchoCNOBridge where
28+
module Echo.Bridges.EchoCNOBridge where
2929

30-
open import Echo
30+
open import Echo.Core
3131

3232
open import CNO using
3333
( Program

0 commit comments

Comments
 (0)