Synthetic forward

The headline case: a cash-settled forward and a long call / short put at the same strike produce exactly the same payoff.

EQUIVALENT executable

Equivalent under the displayed assumptions.

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

Structures compared

Target structure

the exposure you described · 1 leg

Structure legs
Leg	Side	Qty	Instrument	Strike	Amount	Mult.
1	Buy	1	Forward	100	n/a	1

Candidate structure

Candidate: long Call(100) / short Put(100) · 2 legs

Structure legs
Leg	Side	Qty	Instrument	Strike	Amount	Mult.
1	Buy	1	Call	100	n/a	1
2	Sell	1	Put	100	n/a	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
0 <= S < 100	S − 100	S − 100	0
S >= 100	S − 100	S − 100	0

Proof explanation

0 <= S < 100: + Forward(K=100) = S − 100 and + Call(K=100) − Put(K=100) = S − 100 -> difference 0
S >= 100: + Forward(K=100) = S − 100 and + Call(K=100) − Put(K=100) = S − 100 -> 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

+ Call(K=100) − Put(K=100)

Estimated cost: 2.10 USD
vs target: −0.25 USD
Rank: #1
Provenance: supplied candidate

Interval evidence, metadata gate and cost detail

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff	Difference
0 <= S < 100	S − 100	S − 100	0
S >= 100	S − 100	S − 100	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_AVAILABLE

2.10 USD estimated entry cost, fees included

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Call(K=100)	BUY	11.45	0.05	11.50
− Put(K=100)	SELL	9.45	0.05	−9.40

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 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

2 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

2.35 USD estimated entry cost, fees included

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Forward(K=100)	BUY	2.30	0.05	2.35

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 A cheaper	2.10 USD	−0.25 USD

Alternative A is cheaper than the target by 0.25 USD under the supplied quotes.

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.

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.