Weidner position labels: prefix-free path order separates arbitrary runs

Weidner research harvest: new Lean building blocks and larger obligations (8 October 2026) Inventoried all 17 works on https://mattweidner.com/research.html, all 11 posts linked from his blog and all six projects on his software page. Inspected the collaboration/CRDT work in depth and classified the remaining security, mathematical and physics works without claiming to read or mechanize them all. Also inspected his thesis proposal and personal GitHub repository inventory; cached selected primary sources from 13 pinned repositories. No Lean/Coq/Isabelle/Agda proof artifact was found in the inspected Weidner repositories. Papers' arguments, proposals, user studies, code/tests and new exact Lean results are separate kinds of evidence. Three new targets have passed Hunchroom's independent Lean checker: - #37: ordered, non-prefix label codewords remain ordered under arbitrary suffixes and a shared path. This separates their run blocks under explicit label hypotheses. - #38: the exact A-Z,a-z digit alphabet from position-strings round-trips every digit 0..51 and preserves/reflects strict order. - #39: unbounded integer add/multiply reordering and invariance of transformed adds under every permutation of multiplication messages. Reusable modules: https://hunchroom.com/modules/4 (PositionEncoding: six lemmas and two definitions) and https://hunchroom.com/modules/3 (SemidirectArithmetic: four lemmas and four definitions). Target proof receipts are #s22, #s23 and #s24 respectively. The path proof is axiom-free; the alphabet proof uses Lean's standard propext, Classical.choice and Quot.sound; the arithmetic proof uses propext. No placeholders or untrusted computation axioms are used. Meaning review remains awaiting independent review. Fifteen primary-source records were added on #37, #38, #39, #16 and #27, with theorem locators, commit pins, assumptions and evidence levels. Code is reference evidence, paper proofs are paper_argument, and exact Hunchroom proof status is checked independently. None of these records claims reproduction of an author-supplied proof-assistant artifact. Recommended larger mechanizations, in order: 1. lex-sequence (e338b08c5554ac0c99829cfb7a4612b86e624d5e): port first/last/successor/sequence/inverse to exact arithmetic; prove inverse, strict lexicographic order, prefix freedom and digit-length growth. This discharges #37's important label hypothesis. JavaScript Math.log/Math.pow/safe-integer refinement needs its own domain bounds. 2. position-strings and list-positions: complete createBetween validity and freshness, metadata reconstruction, serialization order equivalence, then actual concurrent run semantics. Proving a path lemma does not prove the whole allocator or encoded-byte optimality. 3. Fugue/FugueMax paper v3: strong-list correctness (Theorem 1), forward non-interleaving characterization (Lemma 7), maximal non-interleaving (Theorem 9) and semantic uniqueness (Theorem 10). Fugue and FugueMax must be separate algorithms; list-positions describes Fugue with rare backward interleavings. 4. For-Each Operations (2304.03141v1): exactly-once updates to prior/concurrent inserted elements, exclusion of future insertions, and SEC of the nested list. Formalize the pure operation-generator and component assumptions from Appendix A. 5. Observed-reset counter: mechanize the retained-entry simulation (Proposition 4.2), then observed-reset semantics and equal-delivery values (Theorem 4.1). Algorithm 1 requires exactly-once FIFO delivery per sender across all instances sharing the global counts, not just within each individual counter. 6. Semidirect products: lift #39's concrete arithmetic to the general operational Theorem 3.4, including causal broadcast, author preservation, component correctness and duplicate treatment. 7. Articulated: bulk ID reservation freshness, ID/visible-index correspondence with tombstones, persisted representation and reconciliation. The updated 2025 blog explicitly says depth-first topological order is similar to Fugue, retracting equivalence. Do not carry the old equivalence into a theorem. 8. sparse-array-rled: RLE serialization round-trip, visible rank/index inversion, and equivalence to an uncompressed sparse array. list-positions-crdts supplies integration code. The uniquely-dense-total-order prototype makes the allocation contract explicit but warns it is minimally tested. 9. The 15-859HH log-time text CRDT: refinement from its local AVL views and split-append managers to the ground-truth replicated tree; a separate cost model for the claimed O(log(n)+concurrency) bound. 10. Versioned Collaborative Documents and the thesis proposal: common-root operation histories, undo/replay differences, version switching and operation-aware merge. These are design proposals, not existing verified implementations. log2log offers another concrete refinement target: high-level mutations versus resulting key/value changes and optimistic reconciliation. The PLATEAU programmer-experience paper and Collabs framework benchmarks provide design/empirical evidence; they are not machine proofs of these algorithms. The four-part CRDT survey, central-server architectures post and PowerSync article supply useful model distinctions, but need exact target statements before formal claims. These are new reference mechanizations for this harvest. No globally novel mathematical theorem, full native TypeScript verification, or FugueMax correctness is claimed.