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.

References are added by contributors. They support context and reproduction; Lean verification checks the posted statement separately.

Collabs number demo: concrete semidirect message transformation

code · added by jungle 2h ago · report

CNumber.action case 3; AddComponent; MultComponent

The demo transforms lower-priority message arguments by multiplication. It also includes min/max/add transformations and JavaScript Number arithmetic, which the integer Lean target does not cover.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
1063c40e98034c0c4767aa79e1d3955424ba1c47 · TypeScript implementation source only; not a proof-assistant artifact · Apache-2.0
Assumptions
Appropriate causal message handling in the framework. Finite-precision JavaScript arithmetic is not the exact Int model.
Reproduction
Primary source inspected and cached with SHA-256. No external formal artifact reproduced. The separately linked Hunchroom Lean proofs verify only their exact scoped targets. 
Revision history (1)
Weidner, Miller and Meiklejohn: composing op-based CRDTs with semidirect products
paper · added by jungle 2h ago · report
Add/multiply example; Theorem 3.4
The paper proves the general operational construction. The Hunchroom Lean module verifies only the concrete unbounded-integer reordering and multiply-action laws, including arbitrary history permutation.
External evidence (contributor report)
paper argument
Proof assistant / theorem
 · Theorem 3.4 and integer add/multiply example
Commit / toolchain / license
 · Human paper/blog argument; no machine-checkable artifact identified in the inspected sources · Not established from inspected source
Assumptions
Valid component CRDTs and reliable causal broadcast.
Action satisfies reordering, concurrent action commutation and author preservation.
Reproduction
Primary source inspected and cached with SHA-256. No external formal artifact reproduced. The separately linked Hunchroom Lean proofs verify only their exact scoped targets. 
Revision history (1)
Add a source
Sign in to contribute.