Chambers

The information most worth computing on is private, and it stays uncomputed because it cannot be broadcast: which two people should meet, who should hire whom, which lab has a technique another would pay for, what a decade of someone's notes says about them. The common workaround is to upload it all to a platform and trust the platform, which hands a lifetime of context to someone else's model.

A chamber is a computation confined to the private worlds it has touched. Around it runs a market in which the tradable good is a bounded computation right, the deliverable is one symbol from a closed alphabet, the price system is a lifetime exposure ledger, and settlement is recorded in a court file. A buyer receives a scoped right and legible evidence of what was computed; the underlying data does not change hands.

Clearing: leakage to any observer coalition is at most the sum of charges on the crossings that reach it — provided every observable is enumerated and every schedule is fixed or public-computable. Clearing is a specification enforced by kernel and review; its soundness proof is an open goal recorded by name. Free post-processing: released symbols are public values; any function of them charges nothing.

The refusals carry weight in the design. A type may name an unsolved problem and record it as unprovable; it may not assert the problem away with a boolean. The laws draw on named literatures (quantitative information flow and g-leakage, differential-privacy odometers, contextual integrity, Certificate Transparency, peer prediction, Shapley valuation), cited law by law in the repository. Four of the fourteen refusals:

• Identityuniqueness is unsolved; every per-entity key is Sybil-soft, and the ledger shows the undercount it cannot prevent
• Harmthe meter prices channel width and says nothing about damage; a single bit can do unbounded harm
• Trusted coreoperator, verifiers, reviewers, and hardware roots remain trusted parties; the ledger records them and does not remove them
• Declared channelswhere no alphabet closes, the meter bounds what the ledger records and does not bound the adversary

The accounting layer runs and is cross-verified. A Python reference and a Rust twin written from the spec alone agree bit-for-bit on all 195 conformance decisions across 31 golden traces, which is possible because no float is in the decision path. One author wrote both, with the reference sealed during the port. The charge algebra's theorems (ceiling law, global cap under lease partition, settlement conservation, widening one-way-ness) are machine-checked in Lean 4, with golden traces from the reference replayed inside the proofs. All three floors verify in public CI.

python3 -m pytest -q                          # the whole floor
python3 -m chambers.pipeline.run_pipeline     # nine machines as one system
cd chambers/kernel/rust_ledger && cargo test  # the counterparty's verifier
cd chambers/lean && lake build                # the proof kernel

Chambers is a substrate with its evidence; there is no hosted product. The operator-observed and reproducible-local assurance rungs exist. TEE attestation is in the design and unbuilt, and the soundness proof connecting the type system to quantitative information flow is the open goal named above. The repository's IP manifest states exactly what the release gives and withholds.

The code, the Book, the specs, and the golden corpora are public at github.com/XyraSinclair/private-data-computation-protocol under the Harvest License. You may use, fork, or sell it; at most once a year the steward may ask what it has been worth to you, and any honest answer satisfies the license in full. A reported conformance divergence or spec ambiguity is a contribution, and a reimplementation of the decision core by someone other than its author is the standing invitation.