{"version":3,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"std","imports":["Std","Batteries","Lean.Elab.Tactic.Omega"],"statement_hash":"b2cd1bc58c5fcec7c92e0003ed433e5aed4dc5a35e4acdfe0610844fbc0da0e4","problem":{"id":37,"title":"Weidner position labels: prefix-free path order separates arbitrary runs","description":"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.","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))","profile":"std","module_pins":[{"id":4,"hash":"adeffaae5c39158df4a8f2822fbb1bff2a653526063435d91ff76f0081faac0b"}],"module_context":[{"id":4,"hash":"adeffaae5c39158df4a8f2822fbb1bff2a653526063435d91ff76f0081faac0b","namespace":"PositionEncoding","source":"namespace Hunch.PositionEncoding\ndef digitCode : (Nat → Nat) :=\n  fun d => if d < 26 then 65 + d else 71 + d\n\ndef parseDigit : (Nat → Nat) :=\n  fun c => c - (if c ≥ 97 then 71 else 65)\n\ntheorem digit_roundtrip : (∀ d : Nat, d < 52 → parseDigit (digitCode d) = d) :=\n  by\n    intro d hd\n    unfold parseDigit digitCode\n    split <;> split <;> omega\n\ntheorem digit_order : (∀ a b : Nat, a < 52 → b < 52 → (digitCode a < digitCode b ↔ a < b)) :=\n  by\n    intro a b ha hb\n    unfold digitCode\n    split <;> split <;> omega\n\ntheorem common_prefix : (∀ (stem xs ys : List Nat), List.Lex (· < ·) xs ys → List.Lex (· < ·) (stem ++ xs) (stem ++ ys)) :=\n  by\n    intro stem xs ys h\n    induction stem with\n    | nil => exact h\n    | cons a stem ih => exact List.Lex.cons ih\n\ntheorem suffix_stable : (∀ (xs ys leftTail rightTail : List Nat), List.Lex (· < ·) xs ys → (¬ ∃ tail : List Nat, ys = xs ++ tail) → List.Lex (· < ·) (xs ++ leftTail) (ys ++ rightTail)) :=\n  by\n    intro xs ys leftTail rightTail h\n    induction h with\n    | nil =>\n      intro hn\n      exact False.elim (hn ⟨_, rfl⟩)\n    | rel hab =>\n      intro _\n      exact List.Lex.rel hab\n    | cons h ih =>\n      intro hn\n      apply List.Lex.cons\n      apply ih\n      intro hp\n      obtain ⟨tail, eq⟩ := hp\n      apply hn\n      exact ⟨tail, congrArg (List.cons _) eq⟩\n\ntheorem run_separation : (∀ (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))) :=\n  by\n    intro stem leftLabel rightLabel leftRun rightRun h hn\n    exact common_prefix stem _ _ (suffix_stable _ _ _ _ h hn)\n\ntheorem side_bracketing : (∀ (stem tail : List Nat) (n : Nat), List.Lex (· < ·) (stem ++ (2*n :: tail)) (stem ++ [2*n+1]) ∧ List.Lex (· < ·) (stem ++ [2*n+1]) (stem ++ ((2*n+1) :: (0 :: tail)))) :=\n  by\n    intro stem tail n\n    constructor\n    · apply common_prefix\n      apply List.Lex.rel\n      omega\n    · apply common_prefix\n      exact List.Lex.cons List.Lex.nil\n\nend Hunch.PositionEncoding\n"}],"scope":{"obligations":["other"],"assumptions":["Label codewords are strictly ordered; the left codeword is not a prefix of the right."],"cost_metric":"none","model_scope":"Finite paths of natural-number code units; lexicographic first-difference order.","implementation":"","correspondence":"abstract_model","limitations":["Generated position strings, JavaScript string comparison, fresh IDs, code-language prefix freedom, causal delivery and FugueMax remain separate obligations."]}},"source":"import Std\nimport Batteries\nimport Lean.Elab.Tactic.Omega\n\nnamespace Hunch.PositionEncoding\ndef digitCode : (Nat → Nat) :=\n  fun d => if d < 26 then 65 + d else 71 + d\n\ndef parseDigit : (Nat → Nat) :=\n  fun c => c - (if c ≥ 97 then 71 else 65)\n\ntheorem digit_roundtrip : (∀ d : Nat, d < 52 → parseDigit (digitCode d) = d) :=\n  by\n    intro d hd\n    unfold parseDigit digitCode\n    split <;> split <;> omega\n\ntheorem digit_order : (∀ a b : Nat, a < 52 → b < 52 → (digitCode a < digitCode b ↔ a < b)) :=\n  by\n    intro a b ha hb\n    unfold digitCode\n    split <;> split <;> omega\n\ntheorem common_prefix : (∀ (stem xs ys : List Nat), List.Lex (· < ·) xs ys → List.Lex (· < ·) (stem ++ xs) (stem ++ ys)) :=\n  by\n    intro stem xs ys h\n    induction stem with\n    | nil => exact h\n    | cons a stem ih => exact List.Lex.cons ih\n\ntheorem suffix_stable : (∀ (xs ys leftTail rightTail : List Nat), List.Lex (· < ·) xs ys → (¬ ∃ tail : List Nat, ys = xs ++ tail) → List.Lex (· < ·) (xs ++ leftTail) (ys ++ rightTail)) :=\n  by\n    intro xs ys leftTail rightTail h\n    induction h with\n    | nil =>\n      intro hn\n      exact False.elim (hn ⟨_, rfl⟩)\n    | rel hab =>\n      intro _\n      exact List.Lex.rel hab\n    | cons h ih =>\n      intro hn\n      apply List.Lex.cons\n      apply ih\n      intro hp\n      obtain ⟨tail, eq⟩ := hp\n      apply hn\n      exact ⟨tail, congrArg (List.cons _) eq⟩\n\ntheorem run_separation : (∀ (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))) :=\n  by\n    intro stem leftLabel rightLabel leftRun rightRun h hn\n    exact common_prefix stem _ _ (suffix_stable _ _ _ _ h hn)\n\ntheorem side_bracketing : (∀ (stem tail : List Nat) (n : Nat), List.Lex (· < ·) (stem ++ (2*n :: tail)) (stem ++ [2*n+1]) ∧ List.Lex (· < ·) (stem ++ [2*n+1]) (stem ++ ((2*n+1) :: (0 :: tail)))) :=\n  by\n    intro stem tail n\n    constructor\n    · apply common_prefix\n      apply List.Lex.rel\n      omega\n    · apply common_prefix\n      exact List.Lex.cons List.Lex.nil\n\nend Hunch.PositionEncoding\n\ndef OA_statement : Prop := (∀ (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)))\n\n#check OA_statement\n","proof":null}