You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
docs: add skepticisms, paper spine, proof obligations and rewrite README
This completes the conservative repository reorganisation. It adds the explicitly required skepticism documents, the proof obligations ledger, and the short paper spine. The README has been entirely rewritten to introduce the tiny mechanically checked core first, placing all exploratory, bridge, and retracted material under strictly labeled sections. The Justfile is updated to correctly test the new module paths.
Any formalism can be made to work on trivial examples. The true test of a theory is its boundary conditions and where it breaks down.
5
+
6
+
## Explicit Failure Modes
7
+
8
+
1.**Abstraction Leaks:** If users must constantly unwrap the `Echo` to perform standard proofs, the abstraction has failed.
9
+
2.**Combinatorial Explosion:** If composing two lossy operations `f` and `g` results in an unmanageably complex nested `Echo`, the theory is not compositionally viable.
10
+
3.**Triviality:** If the only provable theorems are isomorphic to `f x ≡ f x`, the theory lacks predictive power.
11
+
4.**Lack of Separation:** If the "residue" cannot be meaningfully separated from the full "echo" in a proof-relevant way (e.g., if extracting the constraint requires keeping the entire original witness), then the claim of "partial recovery" is false.
12
+
13
+
## The Burden of Proof
14
+
The repository must provide mechanically checked counter-examples to these failure modes, specifically demonstrating non-trivial composition, manageable complexity, and strict separation of residues.
Yes, structurally, an `Echo` is just a standard homotopy fiber: `Σ A (λ x → f x ≡ y)`. There is no novel syntactic or type-theoretic construction here. If treated purely structurally, there is nothing new.
5
+
6
+
## The Burden of Proof
7
+
The burden of proof lies in demonstrating that treating this specific fiber as a first-class object of study—specifically framing it as "structured loss" or a "retained constraint" over a projection—yields results that are practically obscured when treating it just as a generic pullback over a point.
8
+
9
+
## Collapse Conditions
10
+
If the resulting theorems are identical in both form and usage to standard lemmas about HoTT fibers (e.g., contractibility of fibers for equivalences), then the "Echo" terminology is an unnecessary renaming and should be collapsed back to standard fiber theory.
11
+
12
+
## Reinterpretation vs. Novelty
13
+
The claim is *not* mathematical novelty of the definition. The claim is that identifying this structure as a computational artifact of irreversible processes (rather than just a topological invariant) exposes a class of practically useful "residue" theorems that standard literature ignores.
Yes, at the lowest level of Agda code, this is `Σ (x : A) , (f x ≡ y)`. It relies entirely on the standard dependent pair type and propositional equality.
5
+
6
+
## The Burden of Proof
7
+
Any claim of utility must show why working with the `Echo` wrapper is better than directly pattern-matching on the Sigma type. If every proof immediately unpacks the `Echo` and does standard Sigma-type manipulation, the abstraction is leaky and pointless.
8
+
9
+
## Collapse Conditions
10
+
If the `Echo` interface requires the user to manually manage the underlying `Σ` structure to accomplish basic composition or mapping tasks, the abstraction fails.
11
+
12
+
## Reinterpretation vs. Novelty
13
+
The novelty must reside in the API and the categorical/compositional properties exposed by the wrapper, demonstrating that `Echo` behaves coherently under lossy operations in a way that bare Sigma types do not automatically communicate.
Type theory has had fibers, sigma types, and pullbacks since its inception. Categorical logic has well-understood models for irreversibility.
5
+
6
+
## The Burden of Proof
7
+
We must prove that "Echo Types" provide a formally verified vocabulary for *partial recovery* and *provenance* that is significantly more ergonomic or insightful than existing encodings.
8
+
9
+
## Collapse Conditions
10
+
If the "Echo" approach does not scale to practical examples (like lossy boolean classification or quotienting) without degenerating into unreadable equality proofs, it is not a useful contribution. If it is exactly isomorphic to a known, established approach (e.g., standard refinement types) without offering new insights, it is redundant.
11
+
12
+
## Reinterpretation vs. Novelty
13
+
The mathematical foundation is entirely standard. The potential novelty is the formalisation of "structured loss"—treating the irreversible destruction of information as a first-class object that leaves a proof-relevant, computable residue, rather than merely a forgotten input.
Standard formalisms prioritize reversible or perfectly linear systems where no information is lost, or simply discard lost information entirely in irreversible systems. There is no first-class treatment for *structured* loss where the fact of the loss and a constraint on what was lost are retained.
5
+
6
+
## 2. Observation
7
+
When a non-injective function collapses distinct inputs to the same output, the fiber over that output contains the exact witness of the collapse. Treating this fiber not as a topological artifact but as a computational "echo" provides a formal vocabulary for partial recovery.
8
+
9
+
## 3. Definition
10
+
Given `f : A → B`, the echo at `y : B` is defined as:
11
+
`Echo f y := Σ (x : A) , (f x ≡ y)`
12
+
13
+
## 4. Why ordinary fibers are insufficient
14
+
While structurally identical to homotopy fibers, ordinary fibers are rarely studied as carriers of programmatic provenance or computational residue. The "Echo" vocabulary shifts the focus from equivalence proofs to epistemic constraints and non-injective bounds.
15
+
16
+
## 5. Characteristic theorem candidates
17
+
-`collapse-non-injective`: Explicit witnesses of irreversible collapse.
18
+
-`no-section-visible`: It is impossible to fully reconstruct the input from the output alone.
19
+
-`visible-constraint`: Projection-style structured loss retains a provable constraint on the original state.
20
+
21
+
## 6. Canonical example
22
+
Lossy boolean classification (`true` and `false` collapsing to `unit`), demonstrating distinct echoes over the same visible value.
23
+
24
+
## 7. Failure conditions
25
+
If the echo type requires constant manual unwrapping to the underlying sigma type, or if compositional complexity explodes, the abstraction fails.
26
+
27
+
## 8. Bridge roadmap
28
+
Future exploratory work includes bridging this minimal core to thermodynamic costs, tropical semantics, and choreographic state tracking.
0 commit comments