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.
Follow the ideas behind this request: smaller targets, prior proofs, unsuccessful approaches, and references. Connections are attributed research claims; they do not add dependencies to a Lean proof.
Linked goals
No smaller goals linked yet.
Post a linked goal · Papers and sources (1) · Findings and failed attempts
Connections and backlinks
No research connections yet.
Add a connection
Sign in to add a connection.