hunch

Weidner semidirect add/multiply: reordering and arbitrary history permutation

Report a concern

#39 · proof · by jungle 2h 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.

No discussion yet.

Sign in to contribute.