{"version":3,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"std","imports":["Std","Batteries","Lean.Elab.Tactic.Omega"],"statement_hash":"ed49272ff126428652c11f7f3a2871cdf6847bc99085047e72aa947bc2d029b7","problem":{"id":38,"title":"Weidner base52 alphabet: exact digit round trip and strict order","description":"Reference mechanization of the ASCII A-Z,a-z alphabet used by stringifyBase52/parseBase52 in position-strings. Every valid digit 0..51 round-trips, and the encoder preserves and reflects strict digit order. This is one digit of the codec, not the complete variable-length sequence encoding.","statement":"(∀ d : Nat, d < 52 → Hunch.PositionEncoding.parseDigit (Hunch.PositionEncoding.digitCode d) = d) ∧ (∀ a b : Nat, a < 52 → b < 52 → (Hunch.PositionEncoding.digitCode a < Hunch.PositionEncoding.digitCode b ↔ a < b))","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":["codec_round_trip"],"assumptions":["Digit inputs are natural numbers strictly below 52."],"cost_metric":"none","model_scope":"One ASCII digit represented by its natural-number code; exact integer arithmetic.","implementation":"","correspondence":"algorithm_model","limitations":["No whole-string parser, Unicode normalization, variable-length prefix freedom, encoded-size optimality or JavaScript numeric refinement is claimed."]}},"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 := ((∀ d : Nat, d < 52 → Hunch.PositionEncoding.parseDigit (Hunch.PositionEncoding.digitCode d) = d) ∧ (∀ a b : Nat, a < 52 → b < 52 → (Hunch.PositionEncoding.digitCode a < Hunch.PositionEncoding.digitCode b ↔ a < b)))\n\n#check OA_statement\n","proof":null}