Forward spread collapses to cash

A long forward at K=90 against a short forward at K=110 is exactly the dated cash amount m·(110−90). The sign convention is checked by the verifier, not by hand.

EQUIVALENT executable

Equivalent under the displayed assumptions.

Rewrite budget: rule depth <= 3, candidate cap 24, 4 expansions
Candidates found: 4 verified · 0 refused
Quote source: demo fixture
Proof mechanism: exact piecewise identity, no tolerance

Structures compared

Target structure

the exposure you described · 2 legs

Structure legs
Leg	Side	Qty	Instrument	Strike	Amount	Mult.
1	Buy	1	Forward	90	n/a	1
2	Sell	1	Forward	110	n/a	1

Candidate structure

Candidate: Cash(m·(K2−K1)) = Cash(20) · 1 leg

Structure legs
Leg	Side	Qty	Instrument	Strike	Amount	Mult.
1	Buy	1	Cash	n/a	20	1

Exact verification: target vs candidate

Both structures reduce to the same exact linear function on each interval; both are continuous in the fixing, so interval interior agreement covers the endpoints as well. Coefficients are exact rationals.

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff	Difference
S >= 0	20	20	0

Proof explanation

S >= 0: + Forward(K=90) − Forward(K=110) = 20 and + Cash(A=20) = 20 -> difference 0
Every interval reduces to the same exact linear function, and both structures are continuous in S, so the payoffs agree for all supported S >= 0.
This is exact rational arithmetic over the union of both structures' strikes; no sampled value, tolerance, or market price participates.

Metadata gate every equality-relevant dimension must match

Equality-relevant metadata comparison
Dimension	Target	Candidate	Status
Underlying	BTC	BTC	match
Expiry / event time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement currency	USD	USD	match
Fixing / index	BTC-INDEX-30MIN-V1	BTC-INDEX-30MIN-V1	match
Settlement mechanism	CASH_INDEX	CASH_INDEX	match
Rounding rule	NO_ROUNDING_DEMO_V1	NO_ROUNDING_DEMO_V1	match
Multiplier	1	1	match
Multiplier convention	linear-per-underlying:v1	linear-per-underlying:v1	match

Equality is checked on: underlying, expiry, settlement time, settlement currency, fixing / index, settlement mechanism, rounding rule, multiplier and multiplier convention. Any other contract attribute is absent from this demo, not assumed equal.

Candidates from the rewrite library

Each candidate below was produced by a rule and then re-verified by the exact verifier. A rule firing is never treated as a proof, and the cost column never influences the verdict.

A supplied structure EQUIVALENT

+ Cash(A=20)

Estimated cost: COST_UNAVAILABLE
vs target: n/a
Rank: unranked
Provenance: supplied candidate

Interval evidence, metadata gate and cost detail

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff	Difference
S >= 0	20	20	0

Equality-relevant metadata comparison
Dimension	Target	Candidate	Status
Underlying	BTC	BTC	match
Expiry / event time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement currency	USD	USD	match
Fixing / index	BTC-INDEX-30MIN-V1	BTC-INDEX-30MIN-V1	match
Settlement mechanism	CASH_INDEX	CASH_INDEX	match
Rounding rule	NO_ROUNDING_DEMO_V1	NO_ROUNDING_DEMO_V1	match
Multiplier	1	1	match
Multiplier convention	linear-per-underlying:v1	linear-per-underlying:v1	match

Alternative A estimated cost

demo fixture COST_UNAVAILABLE

COST_UNAVAILABLE

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Cash(A=20)	RESIDUAL	n/a	0.00	n/a

No quote for: + Cash(A=20) (dated cash: no entry price). This structure stays COST_UNAVAILABLE and is excluded from cost ranking.

Cost model assumptions and exclusions

No market-impact, depth, or slippage model.
No funding, borrow, margin, collateral, or discounting.
No partial-fill, latency, or atomic-execution guarantee.
No market-data freshness claim: quotes are the fixture or the values you typed.
Not executable pricing. This is a demonstration estimate over supplied quotes.
Dated cash legs are not priced: the demo does not model discounting or funding, so it refuses to claim an entry cost for the residual obligation.
At least one leg has no quote, so the structure is excluded from cost ranking. The specification's nearest code is COST_UNKNOWN (spec line 241); the brief's required display string is COST_UNAVAILABLE.

B D1 Forward(K) <=> Call(K) - Put(K) EQUIVALENT

− Call(K=110) + Forward(K=90) + Put(K=110)

Estimated cost: 18.40 USD
vs target: +7.60 USD
Rank: #1
Provenance: rule depth 1

Interval evidence, metadata gate and cost detail

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff	Difference
0 <= S < 110	20	20	0
S >= 110	20	20	0

Equality-relevant metadata comparison
Dimension	Target	Candidate	Status
Underlying	BTC	BTC	match
Expiry / event time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement currency	USD	USD	match
Fixing / index	BTC-INDEX-30MIN-V1	BTC-INDEX-30MIN-V1	match
Settlement mechanism	CASH_INDEX	CASH_INDEX	match
Rounding rule	NO_ROUNDING_DEMO_V1	NO_ROUNDING_DEMO_V1	match
Multiplier	1	1	match
Multiplier convention	linear-per-underlying:v1	linear-per-underlying:v1	match

Alternative B estimated cost

demo fixture COST_AVAILABLE

18.40 USD estimated entry cost, fees included

Per-leg cost detail
Leg	Side	Price	Fee	Cost
− Call(K=110)	SELL	1.25	0.05	−1.20
+ Forward(K=90)	BUY	10.90	0.05	10.95
+ Put(K=110)	BUY	8.60	0.05	8.65

Cost model assumptions and exclusions

No market-impact, depth, or slippage model.
No funding, borrow, margin, collateral, or discounting.
No partial-fill, latency, or atomic-execution guarantee.
No market-data freshness claim: quotes are the fixture or the values you typed.
Not executable pricing. This is a demonstration estimate over supplied quotes.

C D1 Forward(K) <=> Call(K) - Put(K) EQUIVALENT

+ Call(K=90) − Forward(K=110) − Put(K=90)

Estimated cost: 21.05 USD
vs target: +10.25 USD
Rank: #2
Provenance: rule depth 1

Interval evidence, metadata gate and cost detail

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff	Difference
0 <= S < 90	20	20	0
S >= 90	20	20	0

Equality-relevant metadata comparison
Dimension	Target	Candidate	Status
Underlying	BTC	BTC	match
Expiry / event time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement currency	USD	USD	match
Fixing / index	BTC-INDEX-30MIN-V1	BTC-INDEX-30MIN-V1	match
Settlement mechanism	CASH_INDEX	CASH_INDEX	match
Rounding rule	NO_ROUNDING_DEMO_V1	NO_ROUNDING_DEMO_V1	match
Multiplier	1	1	match
Multiplier convention	linear-per-underlying:v1	linear-per-underlying:v1	match

Alternative C estimated cost

demo fixture COST_AVAILABLE

21.05 USD estimated entry cost, fees included

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Call(K=90)	BUY	21.30	0.05	21.35
− Forward(K=110)	SELL	0.20	0.05	−0.15
− Put(K=90)	SELL	0.20	0.05	−0.15

Cost model assumptions and exclusions

No market-impact, depth, or slippage model.
No funding, borrow, margin, collateral, or discounting.
No partial-fill, latency, or atomic-execution guarantee.
No market-data freshness claim: quotes are the fixture or the values you typed.
Not executable pricing. This is a demonstration estimate over supplied quotes.

D D1 Forward(K) <=> Call(K) - Put(K) -> D1 Forward(K) <=> Call(K) - Put(K) EQUIVALENT

+ Call(K=90) − Call(K=110) − Put(K=90) + Put(K=110)

Estimated cost: 28.65 USD
vs target: +17.85 USD
Rank: #3
Provenance: rule depth 2

Interval evidence, metadata gate and cost detail

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff
0 <= S < 90	20	20
90 <= S < 110	20	20
S >= 110	20	20

Equality-relevant metadata comparison
Dimension	Target	Candidate	Status
Underlying	BTC	BTC	match
Expiry / event time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement time	2026-12-25 08:00 UTC	2026-12-25 08:00 UTC	match
Settlement currency	USD	USD	match
Fixing / index	BTC-INDEX-30MIN-V1	BTC-INDEX-30MIN-V1	match
Settlement mechanism	CASH_INDEX	CASH_INDEX	match
Rounding rule	NO_ROUNDING_DEMO_V1	NO_ROUNDING_DEMO_V1	match
Multiplier	1	1	match
Multiplier convention	linear-per-underlying:v1	linear-per-underlying:v1	match

Alternative D estimated cost

demo fixture COST_AVAILABLE

28.65 USD estimated entry cost, fees included

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Call(K=90)	BUY	21.30	0.05	21.35
− Call(K=110)	SELL	1.25	0.05	−1.20
− Put(K=90)	SELL	0.20	0.05	−0.15
+ Put(K=110)	BUY	8.60	0.05	8.65

Cost model assumptions and exclusions

No market-impact, depth, or slippage model.
No funding, borrow, margin, collateral, or discounting.
No partial-fill, latency, or atomic-execution guarantee.
No market-data freshness claim: quotes are the fixture or the values you typed.
Not executable pricing. This is a demonstration estimate over supplied quotes.

Rewrite premises and budget notes

D4 reverse (Cash -> forward spread) skipped: many strike pairs produce the same cash amount, so the counter-strike is not uniquely inferable and the premise is UNKNOWN (spec lines 867-875 block a rule on UNKNOWN).
D4 Forward(K1) - Forward(K2) <=> Cash(m*(K2-K1)) skipped: fewer than two forward strikes are present, so the premise is FALSE.

Payoff

visualisation · not the proof

5 net payoff curves plotted. They land on the same line, because that is the finding: same payoff, different structures. Dotted curves are the legs of the target and dashed curves are the legs of the plotted representation. Those differ, and they are the comparison.

Difference: target − plotted candidate

Difference between target and the plotted candidate

Δ(S) = 0 exactly on every interval

The flat line at zero in the difference plot is a bug detector over a display grid. The exact interval table above is what decides equivalence.

The chart is a visualisation, not the equivalence proof. Equivalence is decided by the exact piecewise table above it, which compares the two structures on the union of their option strikes using exact rational arithmetic.

Target estimated cost

demo fixture COST_AVAILABLE

10.80 USD estimated entry cost, fees included

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Forward(K=90)	BUY	10.90	0.05	10.95
− Forward(K=110)	SELL	0.20	0.05	−0.15

Cost model assumptions and exclusions

No market-impact, depth, or slippage model.
No funding, borrow, margin, collateral, or discounting.
No partial-fill, latency, or atomic-execution guarantee.
No market-data freshness claim: quotes are the fixture or the values you typed.
Not executable pricing. This is a demonstration estimate over supplied quotes.

Cost ranking

cost-complete structures only

Ranked estimated cost
#	Structure	Estimated cost	vs target
1	Alternative B	18.40 USD	+7.60 USD
2	Alternative C	21.05 USD	+10.25 USD
3	Alternative D	28.65 USD	+17.85 USD

The target is cheaper than every alternative here; the closest is Alternative B, costing 7.60 USD more.

Estimated cost, exact amounts in the table above

Ranking happens only among structures with a complete quote set. Cost is computed after the semantic work and can never change a verdict.

Unranked structure

demo fixture COST_UNAVAILABLE

COST_UNAVAILABLE

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Cash(A=20)	RESIDUAL	n/a	0.00	n/a

No quote for: + Cash(A=20) (dated cash: no entry price). This structure stays COST_UNAVAILABLE and is excluded from cost ranking.

Cost model assumptions and exclusions

No market-impact, depth, or slippage model.
No funding, borrow, margin, collateral, or discounting.
No partial-fill, latency, or atomic-execution guarantee.
No market-data freshness claim: quotes are the fixture or the values you typed.
Not executable pricing. This is a demonstration estimate over supplied quotes.
Dated cash legs are not priced: the demo does not model discounting or funding, so it refuses to claim an entry cost for the residual obligation.
At least one leg has no quote, so the structure is excluded from cost ranking. The specification's nearest code is COST_UNKNOWN (spec line 241); the brief's required display string is COST_UNAVAILABLE.

Cost model scope

No market-impact, depth, or slippage model.
No funding, borrow, margin, collateral, or discounting.
No partial-fill, latency, or atomic-execution guarantee.
No market-data freshness claim: quotes are the fixture or the values you typed.
Not executable pricing. This is a demonstration estimate over supplied quotes.

Would this matter in your workflow?

The most useful thing you can send is a real structure or contract pair from your own book.

Request a design-partner conversation

What this result does not claim

Research and product demonstration. This is not the production FESC system, not a trading system, and not production safe. There is no order execution, no broker connectivity, and no live market data anywhere in this application.
No guaranteed savings, no guaranteed profitability, no legal equivalence, and no complete market coverage is claimed. Cost figures are demonstration estimates over supplied quotes.
The rewrite library is four parity rewrite rules applied within a bounded depth budget, not a complete equality-saturation search.
Equality here is exact within this demo's semantic scope. It is not a Lean-admitted theorem and makes no schedule-independence claim.