# 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)
```