The all-player simulation

The protocol earns an intermediation spread — the gap between what commodity borrowers pay and what on-chain capital expects. The natural next question is whether routing the token through lending markets earns more of that spread.

The answer has two halves that point in opposite directions, which is why it is worth simulating rather than asserting. Both halves are proved in DoreFormal/DefiSim.lean.

All venue coordinates below are unverified: a 3% borrow against an 80% listing, looped five times, with the curator taking a tenth of interest. They are illustrative parameters, not any venue's published terms.

Half one: the venue does pay the protocol

The protocol charges its margin on reserve. A leverage loop manufactures reserve — every leg of the loop buys more of the yield token. So the protocol's booked revenue rises sharply.

Against an unlevered holder the protocol books 450; against the same equity looped, 1,660. The founder's intuition is correct on this half: the_venue_pays_the_protocol_through_size.

The interest is a pure transfer — what the looper pays is exactly what the depositor and curator receive, proved for any venue configuration (venue_interest_is_a_pure_transfer). The distribution layer creates no surplus of its own. It moves surplus and charges for the moving.

And the loop reverses on its own arithmetic when borrowing costs more than the asset yields (the_loop_reverses_when_borrowing_is_dear). No covenant is needed to stop it.

Half two: the loop finances nothing

Reserve is not deployment. At a capacity equal to the unlevered reserve, a five-loop position books 36,892 bps of reserve and still deploys only 10,000 — everything above the cap is a claim on treasuries wearing a commodity-finance label (loop_creates_reserve_not_financing).

Stated generally: real deployed capital never exceeds originated capacity, for any venue configuration whatsoever (rdc_never_exceeds_capacity). There is no loop that finances a trade which was never originated.

The consequence lands on the holder. If the reserve outruns capacity, the marginal dollar cannot be lent against metal, so it sits in treasuries and the blended yield falls — for everyone, not just the looper:

The token still says commodity finance; three quarters of it is now treasuries (looping_past_capacity_dilutes). And when capacity keeps pace, dilution vanishes entirely — so the dilution is a statement about origination, not about leverage (dilution_is_an_origination_limit).

The trap, stated as a theorem

Both halves are true simultaneously, and together they are the design constraint:

At fixed capacity the loop raises the protocol's booked revenue from 450 to 1,660 while the yield actually backing the token falls from 1,200 to 635.

That is the_leverage_trap. A protocol optimising its own revenue line would run this loop. A protocol optimising the holder's position would not.

We publish it because the incentive it describes is ours, and an allocator should be able to see that we know it. The governing rule follows directly: leverage is a distribution feature and must never be the reason the underlying credit appears solvent. Twenty times TVL is not twenty times commodity financing.

What this implies for reporting

Real deployed capital must be reported separately from total value locked and from gross leveraged exposure. A single headline number cannot distinguish the two, and the difference is exactly where a reader would be misled.

The same discipline applies to claim lineage: every derived position must trace back to the underlying claim, and multiple representations of one claim must never be treated as independent collateral. That is the on-chain form of the double-pledge fraud, and it deserves the same intolerance.