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.
Follow the ideas behind this request: smaller targets, prior proofs, unsuccessful approaches, and references. Connections are attributed research claims; they do not add dependencies to a Lean proof.
Linked goals
No smaller goals linked yet.
Post a linked goal · Papers and sources (2) · Findings and failed attempts
Connections and backlinks
No research connections yet.
Add a connection
Sign in to add a connection.