docs(review): add DNA encoding review log — alphabet ordering bug + planned fixes

Code review of 5331d2c / 7327775 / d62ea73.

Critical finding: dna_codec.py uses ATGCBSPZ ordering (biological) instead
of spec-mandated ABCGPSTZ (ASCII), breaking the monotone LUT axiom.
Medium: native_decide usage and fragile conjunction chains in HachimojiLUT.lean.
Minor: optimizer correctness claim caveat, encode_binary_vector docstring.

Full findings in docs/build_logs/2026-06-23_session_dna_encoding_review.md
and ContextStream doc 8ed4ba35.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This commit is contained in:
allaun 2026-06-22 23:11:58 -05:00
parent 789968dd66
commit 8f76698747

View file

@ -0,0 +1,85 @@
# Build Log: 2026-06-23 — DNA Encoding Review & Planned Fixes
## Session Summary
Code review of the DNA encoding commits (`5331d2c`, `7327775`, `d62ea73`) by
Claude Code. Identified one critical bug (alphabet ordering mismatch between
`dna_codec.py` and the formal specs), two medium maintenance issues in
`HachimojiLUT.lean`, and three minor issues. Fixes planned for this session.
---
## Commits Reviewed
| Commit | Message | Status |
|--------|---------|--------|
| `d62ea73` | feat(hachimoji): close binaryLUT_exists + BMCTE bridge | Clean — minor issues only |
| `5331d2c` | feat(dna): unified theory — DNA encoding, epigenetic computation | Critical bug found |
| `7327775` | feat(dna): add remaining source files and surface images | No issues |
---
## Findings
### [CRITICAL] Alphabet ordering mismatch — `python/dna_codec.py`
`dna_codec.py` uses `ATGCBSPZ` ordering (biological order) instead of the
spec-mandated `ABCGPSTZ` (ASCII order). This breaks the core monotonicity axiom:
```
∀ v₁ < v int_to_dna(v) < int_to_dna(v)
```
The entire monotone LUT pipeline (sort-by-DNA = sort-by-energy, CRT
reconciliation, epigenetic optimizer result ordering) is invalid when built on
`dna_codec.py`.
**Fix required:** Update `BITS_TO_BASE`, `HACHIMOJI_BASES`, and all derived
tables in `dna_codec.py` to `ABCGPSTZ` ordering. Regenerate all tests.
### [MEDIUM] `native_decide` usage in `HachimojiLUT.lean`
`canonical_phases_preserved`, `stability_points`, `other_bases_not_stable`, and
position theorems use `native_decide` — kernel-bypassing, not final formal state.
**Fix planned:** Convert to `decide` or explicit proofs.
### [MEDIUM] Fragile conjunction chain in position theorems
`canonical_phases_preserved.2.2.2.2.2.1` etc. are brittle. Should use named
`obtain` destructuring.
### [LOW] `binaryLUT_exists` trivial proof — acknowledged, blocked on spec
Constant-Φ composition table is correct but degenerate. Requires 8×8 composition
semantics to be formally specified before non-trivial proof is possible.
### [LOW] `encode_binary_vector` parameter name misleading
`bits_per_var` means "bases per variable". Function only uses A/P regardless of value.
### [LOW] Epigenetic optimizer correctness claim above n=22
"Match ✓ BEYOND" for n≥24 is misleading — no ground truth exists above n=22.
Should read "local optimum quality unverified above n=22."
---
## Planned Fixes (this session)
| # | File | Change |
|---|------|--------|
| 1 | `python/dna_codec.py` | Correct `BITS_TO_BASE` to `ABCGPSTZ` ordering; update `HACHIMOJI_BASES`, `TM_CONTRIBUTION`, `GC_EQUIVALENT`, `LATIN_TO_GREEK`; regenerate tests |
| 2 | `formal/CoreFormalism/HachimojiLUT.lean` | Replace fragile conjunction chains with named `obtain` destructuring |
| 3 | `formal/CoreFormalism/HachimojiLUT.lean` | Convert `native_decide` to `decide` where feasible |
| 4 | `docs/UNIFIED_THEORY.md` | Add correctness caveat to epigenetic optimizer results table |
| 5 | `python/dna_codec.py` | Fix `encode_binary_vector` docstring |
---
## Build Baseline (pre-fix)
```
HachimojiLUT.lean: 2987 jobs, 0 errors (last recorded)
Python tests: 68 tests, all green (pre-fix; will need regeneration after alphabet fix)
```