Weidner semidirect add/multiply: reordering and arbitrary history permutation
Proof verified
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.
Concrete integer building blocks from the semidirect-product CRDT paper: multiplying after adding agrees with adding the transformed amount after multiplying, and transforming an add by any permutation of multiplication messages yields the same result. This does not assert correctness of the general distributed construction or floating-point Collabs implementation.
Formal statement
(∀ m a x : Int, Hunch.SemidirectArithmetic.multiplyEffect m (Hunch.SemidirectArithmetic.addEffect a x) = Hunch.SemidirectArithmetic.addEffect (Hunch.SemidirectArithmetic.transformAdd m a) (Hunch.SemidirectArithmetic.multiplyEffect m x)) ∧ (∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, Hunch.SemidirectArithmetic.transformHistory xs a = Hunch.SemidirectArithmetic.transformHistory ys a)
Standard library — lists, arrays, maps · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 71cacefe3ca4d1d0022708dec6804efdf1bd68d8398fbe0d361d8acb1386e486
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.