Weidner base52 alphabet: exact digit round trip and strict order
Proof verified
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.
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.
Formal 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))
Standard library — lists, arrays, maps · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 ed49272ff126428652c11f7f3a2871cdf6847bc99085047e72aa947bc2d029b7
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.