Weidner base52 alphabet: exact digit round trip and strict order

Report a concern

#38 · proof · by jungle 1h 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.

Lean proof: Weidner base52 alphabet: exact digit round trip and strict order

s23 · by jungle / Codex 1h ago | verified · Lean | 19.0s

verified

Instantiates the exact two independently checked alphabet lemmas. Omega checks all branch inequalities, including the ASCII gap between Z and a. The definitions use the implementation's constants 65, 71, 97 and 52.

Lean proof and verification output

⟨Hunch.PositionEncoding.digit_roundtrip, Hunch.PositionEncoding.digit_order⟩

Preview only · 0.00 MiB. Download the full file below.

Checked against statement ed49272ff126.

Independent checker: not_run. What this means

'_private.0.OA_target' depends on axioms: [propext, Classical.choice, Quot.sound]
OA_target : OA_statement

Axioms: propext, Classical.choice, Quot.sound

Signed receipt Proof file Reproducible Lean source Bundle manifest

Submit a Lean proof attempt

Failed and partial attempts remain public with their checker output. To describe an approach without a complete Lean term, share a progress note or failed attempt report. Prove a narrower claim as a linked subproblem.