Protocol Squisher

Restarted June 2026. The previous incarnation — roughly thirty-five Rust crates, thirteen analysers, and proofs across six provers, developed January–June 2026 — is archived, complete and unedited, in provenance/. See provenance/PROVENANCE.adoc for what it was, what it established, and where it failed.

The three threads

• The field. Moving data between serialization formats is manual and lossy, and the tooling that exists answers compatibility as a binary yes/no — too coarse to act on.

• The theory challenge. Can compatibility be graded rather than declared — can the loss in a conversion be measured, and composed along a chain of them?

• The practical challenge. Can adapters be synthesised automatically, with the loss they incur documented, at a fidelity worth using?

What is settled

The universal-interoperability claim is closed. Transport-class composition is max — a path is only as good as its worst step — so any route through a shared hub is capped by that hub’s worst embedding. "Universal" and "high fidelity" are therefore contradictory the moment any format embeds into the hub at less than perfect grade; universal low fidelity is what JSON already is. This is the hub_ceiling corollary, machine-checked under Lean 4.13.0: provenance/proofs/tropical/TropicalAdapterPath.lean.

What this repo is now

Terminated as an active project (2026-07-06). The universal-interoperability goal is closed — see the hub_ceiling corollary above. The v1.x work is archived, complete and unedited, in provenance/. This repo is frozen as its own provenance and negative result: the Lean proof and the transport-class-lattice paper stand as the contribution. There is no protocol-squisher v2.

Where the living questions went

The three threads did not die with the universal claim — they migrated into the estate’s joinery layer:

• Graded compatibility — loss measured, not declared as a yes/no — is `cleave’s ordinal fidelity (WF/OF): what is preserved vs knowably traded across an interface.

• max / tropical composition of loss is the same max-plus algebra as cleave’s well-founded staircase and the estate’s `tropical-resource-typing.

• A practical data-form that sidesteps the universal trap is spline — a thin alignment over what consumers already speak (Bebop control, WebRTC media), explicitly not a universal hub. spline carries the squisher caution: take the lessons, not the code.

Empirical evidence continues in protocol-squisher.