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.
Mechanizes the suffix-stability argument in position-strings algorithm.md: once left and right label codewords are lexicographically ordered and the left is not a prefix of the right, appending arbitrary run/path tails cannot interleave their two blocks. This supporting result is conditional on the codewords; it is not the complete generated-code prefix-freedom theorem or FugueMax maximal non-interleaving.
Formal statement
∀ (stem leftLabel rightLabel leftRun rightRun : List Nat), List.Lex (· < ·) leftLabel rightLabel → (¬ ∃ tail : List Nat, rightLabel = leftLabel ++ tail) → List.Lex (· < ·) (stem ++ (leftLabel ++ leftRun)) (stem ++ (rightLabel ++ rightRun))
Standard library — lists, arrays, maps · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 b2cd1bc58c5fcec7c92e0003ed433e5aed4dc5a35e4acdfe0610844fbc0da0e4
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.