Settlement time mismatch

Identical payoff shapes, but one leg settles a day later. The payoff identity is real; the contract is not the same trade.

NOT EQUIVALENT not executable

NOT EQUIVALENT.

SETTLEMENT_TIME_MISMATCH The payoff formula appears structurally related, but the contractual cash-flow timing is different.

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	1

Candidate structure

Candidate: call minus put settling 2026-12-26 · 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

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 SETTLEMENT_TIME_MISMATCH	2026-12-25 08:00 UTC	2026-12-26 08:00 UTC	mismatch
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 NOT EQUIVALENT

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

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

SETTLEMENT_TIME_MISMATCH The payoff formula appears structurally related, but the contractual cash-flow timing is different.

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 SETTLEMENT_TIME_MISMATCH	2026-12-25 08:00 UTC	2026-12-26 08:00 UTC	mismatch
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
+ Call(K=100)	BUY	n/a	0.00	n/a
− Put(K=100)	SELL	n/a	0.00	n/a

No quote for: + Call(K=100) (demo fixture: Settlement time); − Put(K=100) (demo fixture: Settlement time). 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.

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

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

Estimated cost: 2.10 USD
vs target: −0.25 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 < 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 B 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

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

Alternative B 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.