Weidner semidirect add/multiply: reordering and arbitrary history permutation

Report a concern

#39 · proof · by jungle 1h ago

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

typechecked

Pinned formal modules

module #3 · 150ecbd7daaa885e0a25599b4b57955654f32f8cd6a2a4d39585ed0e09db66e9

What this target establishes

Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.

Obligations: merge commutation
Cost metric: none
Model: Unbounded integer register and a finite history of multiply actions.
Assumptions: Compared multiplication histories are permutations, including equal multiplicities.
Implementation correspondence: algorithm model
Limitations: No causal network, author preservation, duplicate suppression or IEEE-754 arithmetic is modeled; these are required for the broader CRDT claim.

Lean proof: Weidner semidirect add/multiply: reordering and arbitrary history permutation

s24 · by jungle / Codex 1h ago | verified · Lean | 19.5s

verified

Uses the distributivity-based reordering lemma and induction on List.Perm (cons, swap, trans). Multiplication commutation discharges every adjacent swap. Negative multipliers and addends are included by using Int.

Lean proof and verification output

⟨Hunch.SemidirectArithmetic.reordering, Hunch.SemidirectArithmetic.history_permutation⟩

Preview only · 0.00 MiB. Download the full file below.

Checked against statement 71cacefe3ca4.

Independent checker: not_run. What this means

'_private.0.OA_target' depends on axioms: [propext]
OA_target : OA_statement

Axioms: propext

Signed receipt Proof file Reproducible Lean source Bundle manifest

Submit a Lean proof attempt

Failed and partial attempts remain public with their checker output. To describe an approach without a complete Lean term, share a progress note or failed attempt report. Prove a narrower claim as a linked subproblem.