From 8f766987475f8b4aeb24a74ca41725afed359417 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Mon, 22 Jun 2026 23:11:58 -0500
Subject: [PATCH] =?UTF-8?q?docs(review):=20add=20DNA=20encoding=20review?=
 =?UTF-8?q?=20log=20=E2=80=94=20alphabet=20ordering=20bug=20+=20planned=20?=
 =?UTF-8?q?fixes?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 .../2026-06-23_session_dna_encoding_review.md | 85 +++++++++++++++++++
 1 file changed, 85 insertions(+)
 create mode 100644 docs/build_logs/2026-06-23_session_dna_encoding_review.md

diff --git a/docs/build_logs/2026-06-23_session_dna_encoding_review.md b/docs/build_logs/2026-06-23_session_dna_encoding_review.md
new file mode 100644
index 00000000..deb02ee3
--- /dev/null
+++ b/docs/build_logs/2026-06-23_session_dna_encoding_review.md
@@ -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)
+```