What is proved, and what is not
The Doré formal development is a Lean 4 project of 81 build targets with no
sorry, no admit, no custom axioms and no native_decide. Every result
below is machine-checked. Every limitation below is recorded in the source
itself, not only here.
Proved
The kernel. Money moves between named parties and is neither created nor
destroyed (roster_cash_zero_sum). A facility cannot settle before it is due
(settlement_never_premature) — a rule that was recorded but unenforced until
an external review rejected the corpus over it. A settlement writes a receipt
naming who actually collected, and no later reassignment can rewrite it
(link_violation_immune_to_reassignment).
The economics. The thirteen players' payoffs sum to real production margin
plus external carry minus real cost — every internal transfer cancels
(surplus_identity). With no production and no carry, the players cannot
collectively gain (no_surplus_without_production). The protocol's coordinate
in that ledger is the objective the ceiling maximizes
(protocol_payoff_agrees).
The design. Over the declared class, the participation-feasible optimum is
identified, and the constraints that bind at it are named: the borrower's
participation sets the price, the holder's sets the pass-through, loss
absorption stops the advance. Paying any player above its outside option costs
exactly the excess and buys nothing (holder_slack_is_pure_transfer), so
tightness is forced rather than assumed.
The law. drUSD satisfies the fiat-referenced-token definition mechanically
on sourced text (drusd_meets_frt_definition); sdrUSD satisfies the
collective-investment-fund definition (sdrusd_meets_cif_definition). A
sub-100% design fails the minimum-value rule outright. Holders rank first in
liquidation, capped at par.
Not proved — and why it matters
No architecture is legally feasible today. This is unconditional and holds
for every design in the grammar: the permission is not granted. Optimization
cannot launder an open legal question, and there is a theorem saying so
(no_architecture_legally_feasible_today).
The optima are grid optima. The design space is a bounded, enumerated grid. No continuous claim is made anywhere without a separate approximation bound, and none is proved.
The evaluator is a declared one-period model. Seven shock coordinates are
read by nothing (eval_arch_ignores_unmodeled_coords). Market closure is an
explicit omission. Basis risk is the entire price channel for a hedged design.
Most economic inputs are unverified. Two calibration coordinates are sourced to the deck; nine are not. Every player's outside option is unverified — none is disclosed anywhere. Results depending on them are reported as frontiers, not conclusions. See The physical pipeline for the sharpest example.
No comparison to other protocols exists. Nothing here proves Doré is better than any alternative. No competitor is modeled.