Weidner position encoding: alphabet, prefix-free paths and run separation

Module verified

verified

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.

Namespace: Hunch.PositionEncoding

SHA-256: adeffaae5c39158df4a8f2822fbb1bff2a653526063435d91ff76f0081faac0b

Definitions and named lemmas

namespace Hunch.PositionEncoding
def digitCode : (Nat → Nat) :=
  fun d => if d < 26 then 65 + d else 71 + d

def parseDigit : (Nat → Nat) :=
  fun c => c - (if c ≥ 97 then 71 else 65)

theorem digit_roundtrip : (∀ d : Nat, d < 52 → parseDigit (digitCode d) = d) :=
  by
    intro d hd
    unfold parseDigit digitCode
    split <;> split <;> omega

theorem digit_order : (∀ a b : Nat, a < 52 → b < 52 → (digitCode a < digitCode b ↔ a < b)) :=
  by
    intro a b ha hb
    unfold digitCode
    split <;> split <;> omega

theorem common_prefix : (∀ (stem xs ys : List Nat), List.Lex (· < ·) xs ys → List.Lex (· < ·) (stem ++ xs) (stem ++ ys)) :=
  by
    intro stem xs ys h
    induction stem with
    | nil => exact h
    | cons a stem ih => exact List.Lex.cons ih

theorem suffix_stable : (∀ (xs ys leftTail rightTail : List Nat), List.Lex (· < ·) xs ys → (¬ ∃ tail : List Nat, ys = xs ++ tail) → List.Lex (· < ·) (xs ++ leftTail) (ys ++ rightTail)) :=
  by
    intro xs ys leftTail rightTail h
    induction h with
    | nil =>
      intro hn
      exact False.elim (hn ⟨_, rfl⟩)
    | rel hab =>
      intro _
      exact List.Lex.rel hab
    | cons h ih =>
      intro hn
      apply List.Lex.cons
      apply ih
      intro hp
      obtain ⟨tail, eq⟩ := hp
      apply hn
      exact ⟨tail, congrArg (List.cons _) eq⟩

theorem 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))) :=
  by
    intro stem leftLabel rightLabel leftRun rightRun h hn
    exact common_prefix stem _ _ (suffix_stable _ _ _ _ h hn)

theorem 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)))) :=
  by
    intro stem tail n
    constructor
    · apply common_prefix
      apply List.Lex.rel
      omega
    · apply common_prefix
      exact List.Lex.cons List.Lex.nil

end Hunch.PositionEncoding

Reproducible verification bundle · Signed receipt · Verification guide

Report module

Checker output

'_private.0.Hunch.PositionEncoding.digitCode' does not depend on any axioms
'_private.0.Hunch.PositionEncoding.parseDigit' does not depend on any axioms
'_private.0.Hunch.PositionEncoding.digit_roundtrip' depends on axioms: [propext, Quot.sound]
'_private.0.Hunch.PositionEncoding.digit_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'_private.0.Hunch.PositionEncoding.common_prefix' does not depend on any axioms
'_private.0.Hunch.PositionEncoding.suffix_stable' does not depend on any axioms
'_private.0.Hunch.PositionEncoding.run_separation' does not depend on any axioms
'_private.0.Hunch.PositionEncoding.side_bracketing' depends on axioms: [propext, Quot.sound]
'_private.0.OA_target' does not depend on any axioms
OA_target : OA_statement

To use this module, pin {"id":4,"hash":"adeffaae5c39158df4a8f2822fbb1bff2a653526063435d91ff76f0081faac0b"} in your target’s modules array. Only independently verified modules can be used.