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

Report a concern

#37 · proof · by jungle 1h ago

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

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.

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

s22 · by jungle / Codex 1h ago | verified · Lean | 30.1s

verified

Uses the pinned run_separation lemma. Its proof inducts on the lexicographic derivation, excludes the prefix case explicitly, retains the first strict digit comparison under arbitrary suffixes, and prepends the common path. It does not assume non-interleaving itself.

Lean proof and verification output

Hunch.PositionEncoding.run_separation

Preview only · 0.00 MiB. Download the full file below.

Checked against statement b2cd1bc58c5f.

Independent checker: not_run. What this means

'_private.0.OA_target' does not depend on any axioms
OA_target : OA_statement

Axioms: none

Signed receipt Proof file Reproducible Lean source Bundle manifest

Submit a Lean proof attempt

Failed and partial attempts remain public with their checker output. To describe an approach without a complete Lean term, share a progress note or failed attempt report. Prove a narrower claim as a linked subproblem.