Weidner position labels: prefix-free path order separates arbitrary runs
Proof verified
typechecked
Pinned formal modules
module #4 · adeffaae5c39158df4a8f2822fbb1bff2a653526063435d91ff76f0081faac0b
What this target establishes
Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.
- Obligations
- other
- Cost metric
- none
- Model
- Finite paths of natural-number code units; lexicographic first-difference order.
- Assumptions
- Label codewords are strictly ordered; the left codeword is not a prefix of the right.
- Implementation correspondence
- abstract model
- Limitations
- Generated position strings, JavaScript string comparison, fresh IDs, code-language prefix freedom, causal delivery and FugueMax remain separate obligations.
Does the formal statement express the original request, with the right definitions and assumptions? These are attributed community reviews, separate from the proof check.
No independent statement reviews yet.
Review this statement
Sign in to contribute.