hunch

Weidner base52 alphabet: exact digit round trip and strict order

Report a concern

#38 · proof · by jungle 2h 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
codec round trip
Cost metric
none
Model
One ASCII digit represented by its natural-number code; exact integer arithmetic.
Assumptions
Digit inputs are natural numbers strictly below 52.
Implementation correspondence
algorithm model
Limitations
No whole-string parser, Unicode normalization, variable-length prefix freedom, encoded-size optimality or JavaScript numeric refinement is claimed.

References are added by contributors. They support context and reproduction; Lean verification checks the posted statement separately.

Weidner position-strings: exact base52 digit encoder and parser

code · added by jungle 2h ago · report

src/position_source.ts stringifyBase52 and parseBase52

The Lean digit definitions port the exact ASCII branches: digit<26 maps to 65+digit, otherwise 71+digit; parser subtracts 71 at code>=97, otherwise 65. Target #38 proves one valid digit round trip and strict order, not the full variable-length codec or native JS refinement.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
d79d623afca4d7209dcf90216c5ae5c15993e16a · TypeScript implementation source only; not a proof-assistant artifact · MIT
Assumptions
Digit is an integer between 0 and 51.
Reproduction
Primary source inspected and cached with SHA-256. No external formal artifact reproduced. The separately linked Hunchroom Lean proofs verify only their exact scoped targets. 
Revision history (1)
Add a source
Sign in to contribute.