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.
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 (9) · Findings and failed attempts
Connections and backlinks
No research connections yet.
Add a connection
Sign in to add a connection.