SparseArray serialization, present entries and count/index conversion; SparseString; SparseIndices
Supports separate future proofs of RLE serialization round trip, visible-rank/index conversion and equivalence to an uncompressed sparse array. Used by list-positions; no balance/performance proof or native-code correctness claimed.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
77cd46b8e5d57596e9d69a9fe563e73c5f95a440 · TypeScript implementation source only; not a proof-assistant artifact · MIT
Assumptions
Valid serialized runs and nonnegative safe integer indices.
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.
Makes allocation-between and uniqueness explicit as an abstract data-type contract. README warns the prototype was minimally tested and points to Collabs/position-strings for published versions. This is source evidence, not a machine proof.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
274dfa22e9068c2769f6c3b1015d2c745f5e2775 · TypeScript implementation source only; not a proof-assistant artifact · Not established from inspected source
Assumptions
Allocator identity freshness and valid total-order bounds.
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.
The updated post says depth-first topological order gives behavior similar to Fugue, retracting equivalence. Lamport timestamp ordering corresponds to RGA/causal trees. Keep each ordering and server reconciliation model distinct.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
· Human paper/blog argument; no machine-checkable artifact identified in the inspected sources · Not established from inspected source
Assumptions
Stable immutable element IDs; retained tombstones; deterministic operation order.
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.
ElementIdGenerator.generateAfter; IdList and IdListSimple implementations
Proof candidates include disjoint allocated ID intervals, lookup/visible-index correspondence through tombstones, serialization and reconciliation. ID uniqueness and counter range must be explicit; tests/fuzzing do not constitute formal verification.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
2332042a240327c7ade5fd1ba1a367f230b539c1 · TypeScript implementation source only; not a proof-assistant artifact · MIT
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.
Human proofs establish strong-list semantics for Fugue and maximal non-interleaving for FugueMax, including a semantic uniqueness result. They are future Lean obligations, not established by the conditional path-order lemma.
External evidence (contributor report)
paper argument
Proof assistant / theorem
· Theorem 1; Theorem 9; Theorem 10
Commit / toolchain / license
· Human paper/blog argument; no machine-checkable artifact identified in the inspected sources · CC BY 4.0 (arXiv accepted manuscript)
Assumptions
Reliable causal broadcast, globally unique ordered IDs and well-formed insert/delete histories.
FugueMax-specific placement rules for maximal non-interleaving.
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.
Structured bunch IDs, inner indices and parent metadata are serialized using escaped ID delimiters and lex-sequence. Internal documentation identifies Fugue and rare backward interleaving, so it should not be equated with the stronger FugueMax guarantee.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
383b84479594641a8864f43e781382e5be8cd845 · TypeScript implementation source only; not a proof-assistant artifact · MIT
Assumptions
Valid parent metadata and unique bunch IDs.
ASCII escaping and prefix-free sequence encoding.
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.
src/index.ts first, last, successor, sequence, sequenceInvSafe; README About/Misc
A compact, promising next formalization: exact inverse and successor, numeric/lexicographic order, prefix freedom and digit-length bound. Uses Number, Math.log and Math.pow; an unbounded Nat port would need a separate JavaScript safety refinement.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
e338b08c5554ac0c99829cfb7a4612b86e624d5e · TypeScript implementation source only; not a proof-assistant artifact · MIT
Assumptions
Even base at least 4.
Valid sequence members; JavaScript safe integer/precision domain requires explicit bounds.
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.
Position allocation; relation to Fugue; efficiency discussion
Primary explanation of the construction. Treat ordering, uniqueness, non-interleaving and logarithmic growth as separate obligations. The local Lean results are new supporting mechanizations, not a reproduced author proof.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
· Human paper/blog argument; no machine-checkable artifact identified in the inspected sources · Not established from inspected source
Assumptions
Fresh allocator IDs and valid input boundaries.
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.
Supports the suffix-stability and run-separation model. The code alphabet is ported separately; neither the full label language nor createBetween is verified by those targets.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
d79d623afca4d7209dcf90216c5ae5c15993e16a · TypeScript implementation source only; not a proof-assistant artifact · MIT
Assumptions
Valid globally unique IDs; ID syntax excludes delimiters.
Codewords must preserve order and be non-prefix for arbitrary-suffix stability.
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.