Skip to content

Commit 43edf2a

Browse files
hyperpolymathhyperpolymath
committed
chore: complete structural flattening of proofs/agda as per Master Map
1 parent 3345ff9 commit 43edf2a

80 files changed

Lines changed: 1112 additions & 2230 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.Core
6-
open import Echo.Bridges.AntiEcho
5+
open import Echo
6+
open import AntiEcho
77
open import EchoKernel
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
8+
open import EchoCharacteristic
9+
open import EchoResidue
10+
open import EchoExampleAbsInt
11+
open import EchoExampleParser
12+
open import EchoExampleProvenance
13+
open import EchoExamples
1414

15-
open import Echo.Bridges.EchoChoreo
16-
open import Echo.Bridges.EchoEpistemic
15+
open import EchoChoreo
16+
open import EchoEpistemic
1717
open import EchoLinear
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
18+
open import EchoGraded
19+
open import EchoTropical
20+
open import AntiEchoTropical
21+
open import AntiEchoTropicalGeneric
22+
open import EchoIntegration
23+
open import EchoCNOBridge
2424

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
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
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 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)
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)
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 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, ++, [])
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, ++, [])
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 Echo.Bridges.EchoFiberTriangulation
73+
open import EchoFiberTriangulation
7474

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

‎proofs/agda/AntiEcho.agda‎

Lines changed: 46 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,17 +17,25 @@
1717
-- This thin slice lands obligations 1–4 from `coecho.md` §5 (renamed
1818
-- `antiecho-*`): the carrier, per-element disjointness against Echo,
1919
-- introduction from any witnessed miss, and contravariant `map-over`
20-
-- along the source. The partition-with-decidability lemma and the
21-
-- tropical decomposition (Echo × Π AntiEcho ≃ IsArgmin) are deferred
22-
-- to follow-up slices; see `coecho.md` §5 obligations 5–6.
20+
-- along the source. Obligation 5 (the partition-with-decidability
21+
-- lemma) lands below as `antiecho-partition-dec` and the
22+
-- codomain-decidability variant `antiecho-partition-codomain-dec`.
23+
-- Obligation 6 (the tropical decomposition `Echo × Π AntiEcho ≃
24+
-- IsArgmin`) lives in `AntiEchoTropical.agda` (concrete ℕ-scored
25+
-- form) and `AntiEchoTropicalGeneric.agda` (generic-codomain lift
26+
-- over an abstract `OrderedCodomain` interface).
2327

2428
module AntiEcho where
2529

2630
open import Level using (Level; _⊔_)
2731
open import Data.Empty using (⊥)
2832
open import Data.Product.Base using (Σ; _,_)
33+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
2934
open import Function.Base using (_∘_)
3035
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
36+
open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
37+
38+
open import Echo using (Echo)
3139

3240
----------------------------------------------------------------------
3341
-- antiecho-def — the carrier.
@@ -91,3 +99,38 @@ antiecho-map-over :
9199
{f : A → B} {y : B}
92100
(g : A' → A) → AntiEcho (f ∘ g) y → AntiEcho f y
93101
antiecho-map-over g (x , np) = g x , np
102+
103+
----------------------------------------------------------------------
104+
-- antiecho-partition-dec — every source element classifies to one
105+
-- side, given decidability of `f x ≡ y`.
106+
--
107+
-- The companion to `antiecho-disjoint`. Disjointness ruled out
108+
-- `Echo` and `AntiEcho` *coinciding* on a shared `x`; this lemma
109+
-- says that for *any* `x`, decidability of `f x ≡ y` gives an actual
110+
-- classification of `x` into one side or the other. Together they
111+
-- exhibit `A` as the disjoint union of the Echo-side and the
112+
-- AntiEcho-side parameterised by `y`.
113+
--
114+
-- The asymmetric joint statement `Echo f y → AntiEcho f y → ⊥`
115+
-- (where the two sides carry *different* domain witnesses) is
116+
-- genuinely *not* a theorem and is not what is landed here:
117+
-- consider `f : Bool → Bool` with `f true = true` and
118+
-- `f false = false`; both `Echo f true` (via `(true, refl)`) and
119+
-- `AntiEcho f true` (via `(false, false≢true)`) are inhabited, so
120+
-- the joint statement is refuted by the model. The correct content
121+
-- of "obligation 5" is the per-element classification below.
122+
123+
antiecho-partition-dec :
124+
∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
125+
(x : A) → Dec (f x ≡ y) → Echo f y ⊎ AntiEcho f y
126+
antiecho-partition-dec x (yes p) = inj₁ (x , p)
127+
antiecho-partition-dec x (no np) = inj₂ (x , np)
128+
129+
-- Codomain-decidability variant: when *every* `b ≡ y` is decidable
130+
-- (typically because `B` has decidable equality), the classification
131+
-- closes uniformly over `f x`.
132+
133+
antiecho-partition-codomain-dec :
134+
∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
135+
→ (∀ b → Dec (b ≡ y)) → (x : A) → Echo f y ⊎ AntiEcho f y
136+
antiecho-partition-codomain-dec dec? x = antiecho-partition-dec x (dec? _)

proofs/agda/Echo/Bridges/AntiEchoTropical.agda renamed to proofs/agda/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 Echo.Bridges.AntiEchoTropical where
41+
module 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.Core using (Echo)
50-
open import Echo.Bridges.AntiEcho using (AntiEcho)
51-
open import Echo.Bridges.EchoTropical using (Candidate; score; IsArgmin; TropEcho)
49+
open import Echo using (Echo)
50+
open import AntiEcho using (AntiEcho)
51+
open import EchoTropical using (Candidate; score; IsArgmin; TropEcho)
5252

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

proofs/agda/Echo/Bridges/Dyadic.agda renamed to proofs/agda/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 Echo.Bridges.Dyadic where
8+
module Dyadic where
99

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

proofs/agda/Echo/Bridges/DyadicEchoBridge.agda renamed to proofs/agda/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 Echo.Bridges.DyadicEchoBridge where
8+
module DyadicEchoBridge where
99

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

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

0 commit comments

Comments
 (0)