Skip to content

Commit f68b6d6

Browse files
hyperpolymathhyperpolymath
committed
docs adjacency: per-neighbour distinctness notes
Per-neighbour notes for seven neighbours: - quotients - template, strongest case - galois-connections - 2-cell, diagonal correspondence with quotients - refinement-types - truncation, honest tied case for relevant variants - information-flow - truncation against relational; open against type-theoretic IFC - provenance - multiplicity sub-family - modal-type-theories - NEW neighbour identified by gate-3 - hott-fibers - NEW; echo IS the homotopy fiber, win is over truncated form Two argument families framed in the README: - Truncation: echo carries type-data where neighbour carries propositional or single-witness content - 2-cell: natural 2-cells in neighbour frameworks are Sigma-over-preimages The narrow-claim discipline is uniform: every note states the honest narrow distinctness claim up front, identifies the load-bearing structural argument, points to the formal exhibit or flags it as open, and gives explicit retraction conditions.
1 parent 68acde7 commit f68b6d6

9 files changed

Lines changed: 1558 additions & 258 deletions

‎docs/adjacency/INSERTION_NOTE.adoc‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
= Doc surgery: replace the consolidated neighbour section in gate-1-distinct-phenomenon.adoc
2+
3+
[.lead]
4+
This file contains the replacement text for the consolidated
5+
neighbour-theory section in `docs/gate-1-distinct-phenomenon.adoc`.
6+
After applying, the consolidated doc points to the per-neighbour
7+
adjacency directory rather than duplicating the analysis.
8+
9+
== What to remove
10+
11+
In `docs/gate-1-distinct-phenomenon.adoc`, the entire section
12+
titled "Neighbouring theories that already do 'fibers of
13+
non-injective maps'" — including all five sub-sections (Galois,
14+
quotients, IFC, refinements, provenance). This section is
15+
superseded by the per-neighbour adjacency directory.
16+
17+
== What to insert in its place
18+
19+
[source,asciidoc]
20+
----
21+
== Neighbouring theories
22+
23+
Per-neighbour distinctness comparisons live in
24+
`docs/adjacency/`. Each neighbour gets its own file with an
25+
explicit (narrow) distinctness claim, which structural argument
26+
(truncation, 2-cell, multiplicity) is load-bearing, formal
27+
exhibit pointers, and explicit retraction conditions.
28+
29+
The two argument families that emerged from working through the
30+
neighbours individually are framed in `docs/adjacency/README.adoc`.
31+
Briefly:
32+
33+
* *Truncation arguments* (refinement, IFC, provenance, quotients):
34+
echo wins by carrying type-data where the neighbour carries
35+
propositional or single-witness content. Formal certificate is
36+
the family of `echo-not-prop` lemmas in
37+
`proofs/agda/examples/`.
38+
* *2-cell arguments* (quotients, Galois): echo wins because the
39+
natural 2-cell in the neighbour's framework is
40+
Σ-over-preimages-shaped. Formal certificates are
41+
`EchoVsQuotient.Sophisticated.equalizer→echo-pair` and
42+
`EchoVsGalois.Sophisticated.meet→echo-intersection`.
43+
44+
Two neighbours not in the original five-neighbour list are now
45+
also covered:
46+
47+
* *Modal type theories* (QTT, Reed-Pfenning, etc.) — co-extensive
48+
with echo on bare echo in QTT-class systems; recipe-level
49+
distinctness is an open question. See
50+
`docs/adjacency/modal-type-theories.adoc`.
51+
* *HoTT homotopy fibers* — echo IS the homotopy fiber; the win
52+
is over the propositional truncation modality, not over fibers
53+
themselves. See `docs/adjacency/hott-fibers.adoc`.
54+
55+
The files:
56+
57+
[cols="2,3", options="header"]
58+
|===
59+
| File | Neighbour
60+
| `docs/adjacency/quotients.adoc` | Quotient types / setoid quotients
61+
| `docs/adjacency/galois-connections.adoc` | Galois connections / abstract interpretation
62+
| `docs/adjacency/refinement-types.adoc` | Refinement types
63+
| `docs/adjacency/information-flow.adoc` | IFC (Goguen-Meseguer lineage)
64+
| `docs/adjacency/provenance.adoc` | Provenance / data lineage
65+
| `docs/adjacency/modal-type-theories.adoc` | QTT, Reed-Pfenning, adjoint modalities
66+
| `docs/adjacency/hott-fibers.adoc` | HoTT homotopy fibers
67+
|===
68+
69+
The honest summary: gate #1 has a strong consolidated argument
70+
plus formalised obstructions against the two strongest neighbours
71+
(quotients, Galois) plus formalised truncation wins on three
72+
domains (tropical, epistemic, linear). The remaining neighbours
73+
have framed but only-partially-formalised distinctness claims;
74+
see each file for what's done and what's open.
75+
----
76+
77+
== Why this surgery
78+
79+
The consolidated section gave the impression of five symmetric
80+
comparisons, when in fact two neighbours had hundreds of lines of
81+
formalised obstruction work and three had a paragraph each. The
82+
per-neighbour split makes the gaps visible (refinement, IFC,
83+
provenance need their own dedicated formalisation work; modal
84+
type theories and HoTT fibers need to be acknowledged honestly).
85+
86+
The replacement also enforces the *narrow claim* discipline: the
87+
consolidated section's framings of refinement types and HoTT
88+
fibers in particular were broader than the formal exhibits
89+
support. The per-neighbour notes state the narrow defensible
90+
claims and acknowledge the tied/coincident cases explicitly.
91+
92+
== Cross-cutting consequences
93+
94+
After the surgery:
95+
96+
* `roadmap-gates.adoc` already specifies `docs/adjacency/` as the
97+
gate-1 artefact path; the directory now exists. No
98+
`roadmap-gates.adoc` change required.
99+
* `next-questions.adoc` QC.1 (which proposed the split and
100+
asked whether to do it) is closed by the existence of this
101+
directory. The QC.1 entry should be updated in
102+
`next-questions.adoc` to reflect closure.
103+
* The `gate-1-handoff.adoc` cross-lane observations remain as
104+
evidence of how the split was reached; no edit needed.

‎docs/adjacency/README.adoc‎

Lines changed: 197 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -1,86 +1,216 @@
1-
= Adjacency Notes (Gate 1)
1+
= Adjacency notes
22
:toc: macro
3-
:sectnums:
3+
:source-highlighter: rouge
44

55
[.lead]
6-
One note per neighbouring framework, written to discharge Gate 1 of
7-
`roadmap-gates.adoc`: that echo types name a phenomenon not already
8-
covered elsewhere under a different name.
6+
Per-neighbour distinctness comparisons for the gate #1 identity
7+
claim. This directory is the artefact `roadmap-gates.adoc` § Gate 1
8+
specifies. It supersedes the consolidated neighbour-theory section
9+
in `docs/gate-1-distinct-phenomenon.adoc`, which now points here.
10+
11+
The exploration that motivated this directory (and identified the
12+
gaps it fills) is in `docs/integration-audit.adoc` § "Adjacency
13+
exploration".
914

1015
toc::[]
1116

12-
== Gate 1 test, repeated
17+
== The two argument families
1318

14-
For each framework below, the note answers three questions:
19+
Working through the neighbours individually surfaced a structural
20+
observation that the consolidated framing was glossing: the
21+
distinctness arguments fall into two structurally different
22+
families.
1523

16-
. What is the nearest existing construction?
17-
. What do echo types add?
18-
. What do echo types _not_ add?
24+
=== Truncation arguments
1925

20-
A framework *fails* the test if every claimed addition is already
21-
present elsewhere under another name. Gate 1 *fails* if no framework
22-
survives the test — in which case the identity claim is retracted per
23-
`roadmap-gates.adoc`.
26+
Echo wins by carrying *type-data* where the neighbour carries
27+
*propositional* or *single-witness* content. The formal certificate
28+
is the family of `echo-not-prop` lemmas formalised in
29+
`proofs/agda/examples/`:
2430

25-
== Frameworks surveyed
31+
* `TropicalArgmin.echo-not-prop` — three paths, two argmins
32+
* `EpistemicUpdate.echo-not-prop` — eight worlds, four consistent
33+
* `LinearErasure.echo-not-prop` — two annotated types, one erasure
2634

27-
[cols="1,3", options="header"]
28-
|===
29-
| Note | Nearest construction
35+
The general theorem (forwarded as Q2.1 in `next-questions.adoc`):
36+
for non-injective `f : A → B` with at least two distinct preimages
37+
of `y`, `is-prop (Echo f y) → ⊥`. The n=2 special cases are proved;
38+
the general theorem awaits gate-2 evaluation.
39+
40+
Truncation arguments are load-bearing against:
41+
42+
* Refinement types (in propositional-predicate variants like F\*,
43+
Liquid Haskell — see `refinement-types.adoc`)
44+
* Information-flow non-interference (in relational variants — see
45+
`information-flow.adoc`)
46+
* Provenance (in single-witness variants — see `provenance.adoc`)
47+
* Quotient types (which collapse witnesses by construction — see
48+
`quotients.adoc`)
49+
50+
=== 2-cell arguments
51+
52+
Echo wins because the natural 2-cell in the neighbour's framework
53+
is *Σ-over-preimages-shaped*, i.e., already echo-shaped, when
54+
incomparable kernels force a true 2-cell rather than a refinement
55+
map. The formal certificates:
56+
57+
* `EchoVsQuotient.Sophisticated.equalizer→echo-pair` — quotients'
58+
2-categorical encoding's natural 2-cell is the equalizer of two
59+
parallel maps, which IS Σ-over-preimages.
60+
* `EchoVsGalois.Sophisticated.meet→echo-intersection` — abstract
61+
interpretation's natural 2-cell is the meet in the abstraction
62+
lattice, which IS Σ-over-preimages with a paired predicate.
3063

31-
| link:refinement-types.adoc[Refinement types]
32-
| `{ x : A | P x }` subset types with predicate carrier.
64+
Both arguments are sealed against subordinate sub-cases: joins
65+
(`Joins.join-universal`), indexed families with coherence laws
66+
(`IndexedFamilies.s-2-reduction`).
3367

34-
| link:lenses-and-optics.adoc[Lenses and optics]
35-
| get/put pairs with lawful round-tripping.
68+
The diagonal correspondence
69+
(`Sophisticated.meet-on-diagonal→equalizer`) establishes that the
70+
two arguments agree where they overlap: the AI meet specialises to
71+
the quotient equalizer when output values coincide.
3672

37-
| link:hott-fibers.adoc[HoTT fibers]
38-
| `fib f y := Σ x , f x = y` with univalent identity.
73+
2-cell arguments are load-bearing against:
3974

40-
| link:setoid-quotients.adoc[Setoid quotients]
41-
| `(A , ~)` carrier plus equivalence relation.
75+
* Quotient types (`quotients.adoc`)
76+
* Galois connections / abstract interpretation
77+
(`galois-connections.adoc`)
4278

43-
| link:provenance-semirings.adoc[Provenance semirings]
44-
| `K`-annotated tuples tracked through relational algebra.
79+
=== Multiplicity arguments
4580

46-
| link:cubical-systems.adoc[Cubical systems]
47-
| Cubical Agda, `RedPRL`, `redtt`, `cooltt` as higher-dimensional equality frameworks.
81+
A subset of the truncation family worth distinguishing: provenance
82+
specifically tracks *one* source per output rather than truncating
83+
to "some source exists". The win is at non-injective points; the
84+
loss is the same `echo-not-prop`-flavoured certificate but the
85+
neighbour's failure mode is "single-witness selection" rather than
86+
"propositional truncation" per se.
87+
88+
Treated under truncation in `provenance.adoc`, with the
89+
multiplicity-vs-truncation distinction noted explicitly.
90+
91+
=== Where the wins live (summary table)
92+
93+
[cols="2,2,2,2", options="header"]
94+
|===
95+
| Neighbour | Truncation | 2-cell | Notes
96+
97+
| Refinement types
98+
| Wins against propositional-predicate variants (`echo-not-prop`)
99+
| N/A
100+
| Tied with Σ-relevant variants (Agda, Coq) — these *are* echo
101+
102+
| Quotient types
103+
| Wins (quotients collapse witnesses by construction)
104+
| Wins (`equalizer→echo-pair` + S-1, S-2)
105+
| Strongest case; argued on both axes
106+
107+
| Galois / AI
108+
| Partial (Galois is propositional/relational about the abstract domain)
109+
| Wins (`meet→echo-intersection`)
110+
| Diagonal correspondence with quotients
111+
112+
| IFC (Goguen-Meseguer)
113+
| Wins against relational variants (`echo-not-prop` per gate-3)
114+
| Open question against type-theoretic IFC variants
115+
| Genuine open work — see Q2.x candidates
116+
117+
| Provenance
118+
| Wins against single-witness variants (multiplicity)
119+
| Wins (transitive provenance reduces to S-2 case)
120+
| Multiplicity wording is sharper than truncation here
121+
122+
| Modal type theories (QTT, etc.)
123+
| Wins against propositional-mode accounts
124+
| N/A (modal type theories make 2-cells syntactic primitives)
125+
| Co-extensive with QTT-class systems on bare echo; integration recipe is open
126+
127+
| HoTT fibers
128+
| N/A (HoTT fibers are echo by another name)
129+
| N/A (cubical 2-cells are equalizers definitionally)
130+
| Tied; the win is over the propositional-truncation modality, not over HoTT
131+
|===
132+
133+
[NOTE]
134+
====
135+
*EI-2 cascade.* The 2-cell wins above hold on their own structural
136+
terms (equalizers and meets are Σ-over-preimages-shaped). The
137+
*recipe-level* cross-axis commutations on 2D and 3D products are a
138+
*different* story: per the EI-2 investigation
139+
(`docs/EI2_REPORT.adoc`), the integration recipe with the existing
140+
five named axes does *not* produce substantive simultaneous
141+
cross-axis content.
142+
143+
Concretely: across seven data points (sibling 2D constructions
144+
`RoleGraded`, `RoleMode`, `ModeGraded`; the 3D `RoleModeGrade`
145+
with three pairwise commutations and a triple; and the
146+
self-pairing `RoleRole`), every "non-trivial" cell carries
147+
one-axis-at-a-time content, never simultaneous interaction. The
148+
non-loss-only criterion (formal certificate for Choreo in
149+
`ChoreoInjective.agda`) is necessary but not sufficient for
150+
simultaneous interaction; even Role × Role degenerates to either
151+
trivial coordinate-product commutation or breaks the per-axis
152+
transport assumption.
153+
154+
In short: *the integration recipe does not carry the
155+
distinctness load*. The 2-cell argument and the truncation
156+
argument do, and they stand independently.
157+
158+
`gate-1-distinct-phenomenon.adoc` § The Gate #1 claim has been
159+
narrowed to reflect this.
160+
====
161+
162+
== What this directory replaces
163+
164+
The neighbour-theory section in
165+
`gate-1-distinct-phenomenon.adoc` previously listed five neighbours
166+
in a single doc. That section is now superseded by this directory.
167+
The consolidated doc retains the integration-flavoured argument
168+
and the falsification tests T1/T2/T3, but for per-neighbour
169+
comparison work it points here.
170+
171+
The split is per `roadmap-gates.adoc` § Gate 1, which originally
172+
specified `docs/adjacency/` as the gate-1 artefact. The
173+
consolidated form was a transitional state during parallel work;
174+
this directory is the intended structure.
175+
176+
== File index
177+
178+
[cols="2,3", options="header"]
179+
|===
180+
| File | Neighbour
181+
182+
| `quotients.adoc` | Quotient types / setoid quotients
183+
| `galois-connections.adoc` | Galois connections / abstract interpretation
184+
| `refinement-types.adoc` | Refinement types (Σ-relevant and propositional variants)
185+
| `information-flow.adoc` | Information-flow non-interference (Goguen-Meseguer lineage)
186+
| `provenance.adoc` | Provenance / data lineage
187+
| `modal-type-theories.adoc` | QTT, Reed-Pfenning modal calculi, adjoint modalities
188+
| `hott-fibers.adoc` | HoTT homotopy fibers (cubical and Book HoTT)
48189
|===
49190

50-
== Reading order
51-
52-
The notes are independent; read whichever framework you already know and
53-
then cross-check the others. If after reading every note you conclude
54-
that echo types are strictly renamed components of one of these
55-
frameworks, Gate 1 fails and the verdict is recorded in
56-
`docs/retractions.adoc`.
57-
58-
== Scope
59-
60-
All notes are written against the current Agda development
61-
(`--safe --without-K`, no postulates). Claims reference specific
62-
theorems by module and name. Anything not backed by a compiled
63-
theorem is called out as conjectural.
64-
65-
== Compositional evidence (load-bearing across notes)
66-
67-
Three families of theorems in `proofs/agda/Echo.agda` and
68-
`proofs/agda/EchoGraded.agda` are cited across multiple notes as
69-
content distinguishing echo types from neighbours:
70-
71-
* *Base-accumulation iso.* `Echo-comp-iso-{to, from, from-to, to-from}`
72-
proves `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)` with both
73-
round-trips, plus the projection-pentagon lemmas
74-
`Echo-comp-iso-pent-{B, echo}` for three-fold composites.
75-
* *Cancellation under section/retraction.* `cancel-iso-{to, from}`
76-
exhibit `Echo (g ∘ f) y → Echo f (s y)` and back when `g` admits a
77-
pointwise inverse `s`, without needing a triangle-identity coherence
78-
for the partial maps.
79-
* *Per-decoration composition for grades.* `≤g-prop`,
80-
`≤g-⊔g-{left, right, univ}`, `degrade-compose`, `degrade-via-join`
81-
in `EchoGraded.agda` exhibit the grade order as a propositional
82-
pre-order with a categorical join, with degradation composing
83-
uniquely up to `refl`.
84-
85-
Each adjacency note flags whichever of these is load-bearing for its
86-
particular framework comparison.
191+
== What's formalised, what's not
192+
193+
The truncation argument has formal exhibits for three of its
194+
target neighbours via gate-3's `echo-not-prop` family
195+
(`TropicalArgmin`, `EpistemicUpdate`, `LinearErasure`). The
196+
general theorem (Q2.1) is unstated and unproven. Q2.1 is the
197+
single most leveraged open formalisation: closing it would
198+
discharge truncation arguments against all four
199+
truncation-vulnerable neighbours simultaneously.
200+
201+
The 2-cell argument has formal exhibits for both of its target
202+
neighbours (quotients via `EchoVsQuotient.Sophisticated`, Galois
203+
via `EchoVsGalois.Sophisticated`).
204+
205+
The remaining neighbours (IFC, provenance, modal type theories,
206+
HoTT fibers) have prose adjacency notes here but no dedicated
207+
Agda formalisation. Each note states what would be required for
208+
formalisation and forwards the obligation to either Q2.x (for
209+
recipe-level distinctness from a given neighbour) or to Q3.x
210+
(for a canonical example exercising the distinctness).
211+
212+
The honest summary: gate #1 has a strong consolidated argument
213+
plus formalised obstructions against the two strongest neighbours
214+
(quotients, Galois) plus formalised truncation wins on three
215+
domains (tropical, epistemic, linear). The remaining neighbours
216+
have framed but unformalised distinctness claims.

0 commit comments

Comments
 (0)