This milestone ties the C implementation in this repo to the machine-checked proofs in afld-proof.
| Artifact | What it shows |
|---|---|
libdimfold (src/, include/) |
Lossless dimensional folding pipeline: AFLD fold → Fermat bridge → bit-pack |
| Examples & bench | Reproducible round-trip and compression benchmarks on representative vectors |
| afld-proof (sibling repo) | Lean 4 proofs for cyclic preservation, norm preservation, and pipeline bounds — zero sorry in the verified core |
- Systems: C library, fixed-point quantization, performance-oriented bench harness
- Formal methods: Claims in README are backed by a separate proof repo, not hand-wavy docs
- Scientific computing: Targets high-dimensional numerical data where lossy PCA-style methods cap fidelity
# C library
make test && make bench
# Proofs (requires Lean 4 + Mathlib)
cd ../afld-proof && lake build- Publish benchmark numbers with pinned hardware and input fixtures in
bench/ - Narrow public-facing theorem list in afld-proof README to the core compression theorems (see afld-proof sync)