Append-Only Cancellation Ledgers

Abstract

Recording a referenced cancellation preserves the prior ledger and appends one new entry.

Theorem 1.1 (Recording a cancellation is append-only).

$$\forall h,c,\mathrm{prefix}(h,record(h,c))\wedge \mathrm{target}(c)\in record(h,c)\wedge \Vert record(h,c)\Vert =\Vert h\Vert +1.$$

Proof. Machine-checked in Lean as D5/S0/History/CancellationLedger.record_cancellation_is_append_only (✓ std3). ∎

Source. Repository-derived.

Commentary.

A cancellation entry contains a typed index into the existing event history together with the compensating event to record. The index cannot name an absent earlier event. Recording the cancellation retains the complete prior ledger as a prefix, keeps the referenced event present, and increases the ledger length by exactly one. Thus a cancellation changes the running balance through a new audit entry without deleting or rewriting the event it addresses.

Pinned mathlib was searched before proving. Its declarations FreeMonoid.mem_mul, FreeMonoid.length_mul, FreeMonoid.length_of, and List.get_mem supply the complete ledger-theoretic core. No upstream declaration packages a referenced cancellation with all three ledger invariants, so the Lean theorem is a declared thin honest wrapper that combines those laws over the repository’s event history carrier. The source atom contains no numerical certificate.

References

• Truth anchor: D5/S0/History/CancellationLedger.record_cancellation_is_append_only
• Dependency: D5/S0/History/HistoryCarrier