Multiplier mismatch (same cash today)

One lot of the m=2 contract and two lots of the m=1 contract pay the same cash here, but they are different contracts. Only the metadata gate catches it.

NOT EQUIVALENT not executable

NOT EQUIVALENT.

MULTIPLIER_MISMATCH Multiplier conventions differ, so equal underlying moves do not produce equal cash.

Rewrite budget: rule depth <= 3, candidate cap 24, 1 expansions
Candidates found: 1 verified · 1 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	2

Candidate structure

Candidate: 2 lots Forward(100) with multiplier 1 · 1 leg

Structure legs
Leg	Side	Qty	Instrument	Strike	Amount	Mult.
1	Buy	2	Forward	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
S >= 0	2S − 200	2S − 200	0

Proof explanation

The payoff formula appears structurally related, but the equality-relevant metadata differs, so the structures are NOT equivalent.
A payoff identity is only admissible when the contract metadata is identical; the demo holds no rounding/mechanism bridge theorem (spec line 844).

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 MULTIPLIER_MISMATCH	2	1	mismatch
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 NOT EQUIVALENT

+ 2 x Forward(K=100)

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

MULTIPLIER_MISMATCH Multiplier conventions differ, so equal underlying moves do not produce equal cash.

Interval evidence, metadata gate and cost detail

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff	Difference
S >= 0	2S − 200	2S − 200	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 MULTIPLIER_MISMATCH	2	1	mismatch
Multiplier convention	linear-per-underlying:v1	linear-per-underlying:v1	match

Alternative A estimated cost

demo fixture COST_AVAILABLE

4.70 USD estimated entry cost, fees included

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ 2 x Forward(K=100)	BUY	2.30	0.10	4.70

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.

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

+ Call(K=100) [m=2] − Put(K=100) [m=2]

Estimated cost: COST_UNAVAILABLE
vs target: n/a
Rank: unranked
Provenance: rule depth 1

Interval evidence, metadata gate and cost detail

Exact piecewise payoff comparison
Interval	Target payoff	Candidate payoff	Difference
0 <= S < 100	2S − 200	2S − 200	0
S >= 100	2S − 200	2S − 200	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	2	2	match
Multiplier convention	linear-per-underlying:v1	linear-per-underlying:v1	match

Alternative B estimated cost

demo fixture COST_UNAVAILABLE

COST_UNAVAILABLE

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Call(K=100) [m=2]	BUY	n/a	0.00	n/a
− Put(K=100) [m=2]	SELL	n/a	0.00	n/a

No quote for: + Call(K=100) [m=2] (demo fixture: Multiplier); − Put(K=100) [m=2] (demo fixture: Multiplier). 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.
Quotes are bound to the contract they were written for. A leg whose underlying, expiry, settlement, fixing, currency, mechanism, rounding or multiplier differs from the quote source is not priced from it.
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.

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

3 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 payoffs coincide, the refusal is contractual

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_UNAVAILABLE

COST_UNAVAILABLE

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Forward(K=100) [m=2]	BUY	n/a	0.00	n/a

No quote for: + Forward(K=100) [m=2] (demo fixture: Multiplier). 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.
Quotes are bound to the contract they were written for. A leg whose underlying, expiry, settlement, fixing, currency, mechanism, rounding or multiplier differs from the quote source is not priced from it.
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 ranking

no ranked structures

No structure in this comparison had a complete set of quotes, so nothing is ranked.

Unranked structure

demo fixture COST_UNAVAILABLE

COST_UNAVAILABLE

Per-leg cost detail
Leg	Side	Price	Fee	Cost
+ Call(K=100) [m=2]	BUY	n/a	0.00	n/a
− Put(K=100) [m=2]	SELL	n/a	0.00	n/a

No quote for: + Call(K=100) [m=2] (demo fixture: Multiplier); − Put(K=100) [m=2] (demo fixture: Multiplier). 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.
Quotes are bound to the contract they were written for. A leg whose underlying, expiry, settlement, fixing, currency, mechanism, rounding or multiplier differs from the quote source is not priced from it.
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.