SETTLEMENT_MATHEMATICAL_LIFECYCLE_PROOF_MODEL.md

Purpose

Define a mathematical model for settlement lifecycle validity and provide proof sketches for determinism, safety, and authorization soundness.

Scope

Applies to governance-layer settlement reasoning only. The model is ledger-derived and excludes execution-layer side effects.

Definitions

• L = (e_0, e_1, ..., e_n): finite ordered ledger sequence by append index.
• sid: settlement subject identifier, sid = <SubjectType>:<SubjectId>.
• Intent(L, sid): subsequence of entries where recordType=SETTLEMENT_INTENT and subjectId=sid.
• Events(L, sid): subsequence of entries where recordType=SETTLEMENT_EVENT and subjectId=sid.
• Dec(L, sid, a, p): latest ACCESS_DECISION before current point matching (subjectId=sid, action=a, policyHash=p).
• Event type set E = {ESCROW_OPENED, DEPOSIT_CONFIRMED, RELEASE_REQUESTED, RELEASE_EXECUTED, REFUND_EXECUTED, RAIL_ERROR}.

Normative Rules

1. SETTLEMENT_INTENT and SETTLEMENT_EVENT are the only settlement record types.
2. Intent action MUST be SETTLEMENT.CREATE.
3. Event action MUST be SETTLEMENT.<EVENT_TYPE> with <EVENT_TYPE> in E.
4. Validation MUST be computed from L only.

Mathematical Objects

1) Projection Functions

• PI(L, sid) = Intent(L, sid)
• PE(L, sid) = Events(L, sid)

2) Derived State Function

Define S(L, sid) as tuple: (created, escrowOpened, funded, releaseRequestedSet, releasedSet, refunded, railErrorSeen)

Initialization: S_0 = (false, false, false, {}, {}, false, false)

Transition over projected sequence (PI then PE in original ledger order):

• Intent: created := true
• ESCROW_OPENED: escrowOpened := true
• DEPOSIT_CONFIRMED: funded := true
• RELEASE_REQUESTED(m): add m to releaseRequestedSet
• RELEASE_EXECUTED(m): add m to releasedSet
• REFUND_EXECUTED: refunded := true
• RAIL_ERROR: railErrorSeen := true

3) Validity Predicate

V(L, sid) -> (ok: bool, errors: sequence<string>)

ok=true iff all hold:

1. Authorization predicates for intent and each event are satisfied.
2. Ordering constraints are satisfied:
   • if escrowRequired=true then DEPOSIT_CONFIRMED occurs only after ESCROW_OPENED
   • RELEASE_EXECUTED(m) requires prior RELEASE_REQUESTED(m)
   • no RELEASE_REQUESTED or RELEASE_EXECUTED after REFUND_EXECUTED
3. Required event trace metadata exists and matches resolved decision hashes.

Proof Sketches

Theorem 1: Determinism

Statement: For identical ledger L and same verifier rules, S(L, sid) and V(L, sid) are unique.

Sketch:

• L order is total and fixed by append index.
• Projection functions PI, PE are pure filters.
• Transition rules are pure and state-local.
• Authorization lookup Dec is deterministic latest-match scan. Therefore outputs are functionally determined by L.

Theorem 2: Safety (Terminal Consistency)

Statement: If REFUND_EXECUTED exists for sid, no valid state permits later release progression.

Sketch:

• Validity predicate explicitly rejects release actions after refund.
• Any suffix containing release-after-refund produces errors != empty.
• Contradictory terminal outcomes cannot be valid simultaneously.

Theorem 3: Authorization Soundness

Statement: If a settlement event is validly accepted at index k, then there exists earlier matching ALLOW decision and no later matching DENY before k.

Sketch:

• Event authorization is defined by latest-matching decision tuple.
• Latest result must be ALLOW for validity.
• Presence of a later DENY before k would become latest and invalidate event.

Assumptions

1. Ledger entries are immutable once appended.
2. Hash linkage and canonicalization are valid at governance layer.
3. Decision hash fields (authDecisionEntryHash, authDecisionPayloadHash) can be compared exactly.
4. No blockchain consensus or external oracle is required for settlement validity.

Worked Example

Given sid = AUCTION:A-100, policyHash = P-1:

e0: ACCESS_DECISION(ALLOW, action=SETTLEMENT.CREATE, sid, policyHash) e1: SETTLEMENT_INTENT(action=SETTLEMENT.CREATE, sid, policyHash, metadata.escrowRequired=true) e2: ACCESS_DECISION(ALLOW, action=SETTLEMENT.ESCROW_OPENED, sid, policyHash) e3: SETTLEMENT_EVENT(action=SETTLEMENT.ESCROW_OPENED, sid, policyHash, trace hashes) e4: ACCESS_DECISION(ALLOW, action=SETTLEMENT.DEPOSIT_CONFIRMED, sid, policyHash) e5: SETTLEMENT_EVENT(action=SETTLEMENT.DEPOSIT_CONFIRMED, sid, policyHash, trace hashes) e6: ACCESS_DECISION(ALLOW, action=SETTLEMENT.RELEASE_REQUESTED, sid, policyHash) e7: SETTLEMENT_EVENT(action=SETTLEMENT.RELEASE_REQUESTED, sid, policyHash, metadata.milestoneId=M1, trace hashes) e8: ACCESS_DECISION(ALLOW, action=SETTLEMENT.RELEASE_EXECUTED, sid, policyHash) e9: SETTLEMENT_EVENT(action=SETTLEMENT.RELEASE_EXECUTED, sid, policyHash, metadata.milestoneId=M1, trace hashes)

Stepwise state evolution:

• after e1: created=true
• after e3: escrowOpened=true
• after e5: funded=true
• after e7: releaseRequestedSet={M1}
• after e9: releasedSet={M1}

Final result:

• S(L,sid) indicates successful release path without refund.
• V(L,sid) = (true, []).

Mapping to Code

• Intent authorization function: verifySettlementAuthorization.
• Event authorization function: verifySettlementEventAuthorization.
• Lifecycle validity function: verifySettlementLifecycle.
• Model aligns with settlement record builders and appenders in packages/core/settlement/*.

Non-normative Notes

• This model intentionally abstracts storage and transport and focuses on verifiable governance semantics.
• RAIL_ERROR is modeled as a non-terminal event that does not imply fund movement.

Testability

• Determinism tests: replay same L multiple times and across runtimes.
• Safety tests: inject refund then release events and assert invalidity.
• Soundness tests: insert ALLOW then DENY before event and assert deny takes precedence.
• Projection tests: ensure unrelated subjectId entries do not affect S(L,sid).