{"version":3,"kind":"module","module":{"id":4,"user_id":"cef483b5-8f5a-40e6-b0b3-f82d7a8be13a","title":"Weidner position encoding: alphabet, prefix-free paths and run separation","namespace":"PositionEncoding","description":"Lean reference lemmas motivated by position-strings algorithm.md and list-positions. Proves the exact 52-digit ASCII alphabet round trip and ordering, suffix-stable lexicographic order under a non-prefix hypothesis, common-prefix run separation, and left/right natural-number branch bracketing. Does not prove the generated label language is prefix-free, full createBetween, ID freshness, FugueMax, JavaScript number safety, or logarithmic encoded length.","profile":"std","declarations":[{"kind":"definition","name":"digitCode","type":"Nat → Nat","value":"fun d => if d < 26 then 65 + d else 71 + d"},{"kind":"definition","name":"parseDigit","type":"Nat → Nat","value":"fun c => c - (if c ≥ 97 then 71 else 65)"},{"kind":"lemma","name":"digit_roundtrip","type":"∀ d : Nat, d < 52 → parseDigit (digitCode d) = d","value":"by\n  intro d hd\n  unfold parseDigit digitCode\n  split <;> split <;> omega"},{"kind":"lemma","name":"digit_order","type":"∀ a b : Nat, a < 52 → b < 52 → (digitCode a < digitCode b ↔ a < b)","value":"by\n  intro a b ha hb\n  unfold digitCode\n  split <;> split <;> omega"},{"kind":"lemma","name":"common_prefix","type":"∀ (stem xs ys : List Nat), List.Lex (· < ·) xs ys → List.Lex (· < ·) (stem ++ xs) (stem ++ ys)","value":"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"},{"kind":"lemma","name":"suffix_stable","type":"∀ (xs ys leftTail rightTail : List Nat), List.Lex (· < ·) xs ys → (¬ ∃ tail : List Nat, ys = xs ++ tail) → List.Lex (· < ·) (xs ++ leftTail) (ys ++ rightTail)","value":"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⟩"},{"kind":"lemma","name":"run_separation","type":"∀ (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))","value":"by\n  intro stem leftLabel rightLabel leftRun rightRun h hn\n  exact common_prefix stem _ _ (suffix_stable _ _ _ _ h hn)"},{"kind":"lemma","name":"side_bracketing","type":"∀ (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)))","value":"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"}],"module_pins":[],"module_context":[],"module_hash":"adeffaae5c39158df4a8f2822fbb1bff2a653526063435d91ff76f0081faac0b","status":"verified","check_log":"'_private.0.Hunch.PositionEncoding.digitCode' does not depend on any axioms\n'_private.0.Hunch.PositionEncoding.parseDigit' does not depend on any axioms\n'_private.0.Hunch.PositionEncoding.digit_roundtrip' depends on axioms: [propext, Quot.sound]\n'_private.0.Hunch.PositionEncoding.digit_order' depends on axioms: [propext, Classical.choice, Quot.sound]\n'_private.0.Hunch.PositionEncoding.common_prefix' does not depend on any axioms\n'_private.0.Hunch.PositionEncoding.suffix_stable' does not depend on any axioms\n'_private.0.Hunch.PositionEncoding.run_separation' does not depend on any axioms\n'_private.0.Hunch.PositionEncoding.side_bracketing' depends on axioms: [propext, Quot.sound]\n'_private.0.OA_target' does not depend on any axioms\nOA_target : OA_statement","axioms":["propext","Quot.sound","Classical.choice"],"created_at":1791446172,"checked_at":1791446202,"hidden_at":null,"secondary_status":"not_run","secondary_details":null,"origin_submission_id":null,"origin_source_hash":null},"problem":{"statement":"True","profile":"std","module_context":[],"module_pins":[],"module_declarations":[{"kind":"definition","name":"digitCode","type":"Nat → Nat","value":"fun d => if d < 26 then 65 + d else 71 + d"},{"kind":"definition","name":"parseDigit","type":"Nat → Nat","value":"fun c => c - (if c ≥ 97 then 71 else 65)"},{"kind":"lemma","name":"digit_roundtrip","type":"∀ d : Nat, d < 52 → parseDigit (digitCode d) = d","value":"by\n  intro d hd\n  unfold parseDigit digitCode\n  split <;> split <;> omega"},{"kind":"lemma","name":"digit_order","type":"∀ a b : Nat, a < 52 → b < 52 → (digitCode a < digitCode b ↔ a < b)","value":"by\n  intro a b ha hb\n  unfold digitCode\n  split <;> split <;> omega"},{"kind":"lemma","name":"common_prefix","type":"∀ (stem xs ys : List Nat), List.Lex (· < ·) xs ys → List.Lex (· < ·) (stem ++ xs) (stem ++ ys)","value":"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"},{"kind":"lemma","name":"suffix_stable","type":"∀ (xs ys leftTail rightTail : List Nat), List.Lex (· < ·) xs ys → (¬ ∃ tail : List Nat, ys = xs ++ tail) → List.Lex (· < ·) (xs ++ leftTail) (ys ++ rightTail)","value":"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⟩"},{"kind":"lemma","name":"run_separation","type":"∀ (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))","value":"by\n  intro stem leftLabel rightLabel leftRun rightRun h hn\n  exact common_prefix stem _ _ (suffix_stable _ _ _ _ h hn)"},{"kind":"lemma","name":"side_bracketing","type":"∀ (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)))","value":"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"}],"namespace":"PositionEncoding"},"profile":"std","policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","proof":"by trivial","statement_hash":"494cd5346575cc8ca180c5212480b7f23c5adefc25326303724bc72576e2df9d","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 := (True)\n\ntheorem OA_target : OA_statement :=\n  by trivial\n\n#print axioms Hunch.PositionEncoding.digitCode\n#print axioms Hunch.PositionEncoding.parseDigit\n#print axioms Hunch.PositionEncoding.digit_roundtrip\n#print axioms Hunch.PositionEncoding.digit_order\n#print axioms Hunch.PositionEncoding.common_prefix\n#print axioms Hunch.PositionEncoding.suffix_stable\n#print axioms Hunch.PositionEncoding.run_separation\n#print axioms Hunch.PositionEncoding.side_bracketing\n#print axioms OA_target\n#check OA_target\n"}