mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
fix(dna): correct alphabet ordering ATGCBSPZ→ABCGPSTZ + proof cleanup
Critical bug fix: dna_codec.py used biological base ordering (ATGCBSPZ) instead of ASCII-ordered spec ordering (ABCGPSTZ). This violated the core monotonicity axiom (int rank = lexicographic rank) that the entire monotone LUT pipeline depends on. Changes: - python/dna_codec.py: BITS_TO_BASE, HACHIMOJI_BASES, LATIN_TO_GREEK corrected to ABCGPSTZ ordering; encode_binary_vector parameter renamed bases_per_var; module docstring updated - tests/test_dna_codec.py: hardcoded byte→DNA expectations updated for new ordering (0xFF→ZZT, 0xd1→TPC); bases_per_var parameter name updated; 31/31 tests green - formal/CoreFormalism/HachimojiLUT.lean: replace fragile canonical_phases_preserved.2.2.2.2.2.1 chains with named obtain destructuring in pythagorean_position and contradiction_position - docs/UNIFIED_THEORY.md: add ground-truth caveat to epigenetic optimizer results table (n≥24 results are local optima, not verified global minima) Note: test_dna_nn.py has 4 pre-existing failures (Ising chain correlations) unrelated to this fix — dna_qubo_nn.py has its own base encoding and does not import dna_codec.py. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This commit is contained in:
parent
6f55fe0e31
commit
6b649ad271
4 changed files with 52 additions and 39 deletions
|
|
@ -192,12 +192,15 @@ function epigenetic_optimize(Q, n, n_restarts=50):
|
|||
|
||||
| n_vars | Solutions | Brute Force | Epigenetic | Match |
|
||||
|---|---|---|---|---|
|
||||
| 20 | 1M | 0.3s | 0.7s | ✓ |
|
||||
| 22 | 4M | 2.4s | 1.0s | ✓ |
|
||||
| 24 | 16M | FROZEN | 1.5s | BEYOND |
|
||||
| 30 | 1B | FROZEN | 3.4s | BEYOND |
|
||||
| 40 | 1T | FROZEN | 11.3s | BEYOND |
|
||||
| 50 | 1P | FROZEN | 23.9s | BEYOND |
|
||||
| 20 | 1M | 0.3s | 0.7s | ✓ verified vs brute force |
|
||||
| 22 | 4M | 2.4s | 1.0s | ✓ verified vs brute force |
|
||||
| 24 | 16M | FROZEN | 1.5s | local optimum (no ground truth) |
|
||||
| 30 | 1B | FROZEN | 3.4s | local optimum (no ground truth) |
|
||||
| 40 | 1T | FROZEN | 11.3s | local optimum (no ground truth) |
|
||||
| 50 | 1P | FROZEN | 23.9s | local optimum (no ground truth) |
|
||||
|
||||
> **Note:** For n≥24 brute-force enumeration is frozen, so no ground truth exists.
|
||||
> Results above n=22 show convergence to a stable local optimum, not a verified global minimum.
|
||||
|
||||
**Source:** `python/dna_lut.py`, `docs/EPIGENETIC_COMPUTATION.md`
|
||||
|
||||
|
|
|
|||
|
|
@ -347,7 +347,8 @@ theorem pythagorean_position :
|
|||
have hclass : classifyEquation { n_vars := 3, n_ops := 7, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } = StateSigma := by
|
||||
native_decide
|
||||
rw [hclass, canonical_phases_preserved.2.2.2.2.2.1]
|
||||
obtain ⟨-, -, -, -, -, hΣ, -, -⟩ := canonical_phases_preserved
|
||||
rw [hclass, hΣ]
|
||||
|
||||
/-- Contradiction "0 = 1" lives at the Ω (collision) vertex. -/
|
||||
theorem contradiction_position :
|
||||
|
|
@ -358,7 +359,8 @@ theorem contradiction_position :
|
|||
have hclass : classifyEquation { n_vars := 0, n_ops := 0, max_depth := 0,
|
||||
n_quantifiers := 0, n_relations := 1 } = StateΩ := by
|
||||
native_decide
|
||||
rw [hclass, canonical_phases_preserved.2.2.2.2.1]
|
||||
obtain ⟨-, -, -, -, hΩ, -, -, -⟩ := canonical_phases_preserved
|
||||
rw [hclass, hΩ]
|
||||
|
||||
-- ============================================================
|
||||
-- §5 VIRTUAL LUT HIERARCHY
|
||||
|
|
|
|||
|
|
@ -3,12 +3,15 @@
|
|||
dna_codec.py — Hachimoji DNA Encoding/Decoding Layer
|
||||
|
||||
Translates between binary data and Hachimoji 8-base DNA sequences.
|
||||
Uses the SilverSight Hachimoji alphabet (A, T, G, C, B, S, P, Z)
|
||||
Uses the SilverSight Hachimoji alphabet (A, B, C, G, P, S, T, Z)
|
||||
at 3 bits per base — 50% denser than standard 2-bit DNA encoding.
|
||||
|
||||
Encoding table (from HachimojiBase.lean):
|
||||
000 → A (Φ) 001 → T (Λ) 010 → G (Ρ) 011 → C (Κ)
|
||||
100 → B (Ω) 101 → S (Σ) 110 → P (Π) 111 → Z (Ζ)
|
||||
Encoding table (ASCII-ordered, satisfies monotonicity axiom):
|
||||
000 → A (Φ) 001 → B (Λ) 010 → C (Ρ) 011 → G (Κ)
|
||||
100 → P (Ω) 101 → S (Σ) 110 → T (Π) 111 → Z (Ζ)
|
||||
|
||||
ASCII order: A=0x41 < B=0x42 < C=0x43 < G=0x47 < P=0x50 < S=0x53 < T=0x54 < Z=0x5A
|
||||
This guarantees: int_to_dna(v₁) < int_to_dna(v₂) iff v₁ < v₂ (lexicographic = rank).
|
||||
|
||||
Melting temperature contributions (nearest-neighbor simplified):
|
||||
G/C pairs: 3 bonds → high Tm contribution
|
||||
|
|
@ -24,28 +27,29 @@ from typing import List, Tuple
|
|||
# §1 HACHIMOJI ALPHABET
|
||||
# ============================================================
|
||||
|
||||
# 3-bit → base
|
||||
# 3-bit → base (ASCII-ordered: A=0x41 < B=0x42 < C=0x43 < G=0x47 < P=0x50 < S=0x53 < T=0x54 < Z=0x5A)
|
||||
# Monotonicity axiom: int rank = lexicographic rank. Matches HACHIMOJI_DNA_SYNTAX.md and HachimojiLUT.lean.
|
||||
BITS_TO_BASE = {
|
||||
0b000: "A",
|
||||
0b001: "T",
|
||||
0b010: "G",
|
||||
0b011: "C",
|
||||
0b100: "B",
|
||||
0b001: "B",
|
||||
0b010: "C",
|
||||
0b011: "G",
|
||||
0b100: "P",
|
||||
0b101: "S",
|
||||
0b110: "P",
|
||||
0b110: "T",
|
||||
0b111: "Z",
|
||||
}
|
||||
|
||||
# base → 3-bit
|
||||
BASE_TO_BITS = {v: k for k, v in BITS_TO_BASE.items()}
|
||||
|
||||
# All 8 bases in order
|
||||
HACHIMOJI_BASES = list("ATGCBSPZ")
|
||||
# All 8 bases in ASCII order
|
||||
HACHIMOJI_BASES = list("ABCGPSTZ")
|
||||
|
||||
# Greek ↔ Latin (from HachimojiBase.lean)
|
||||
# Greek ↔ Latin (matches HachimojiLUT.lean phase assignments: A=0°=Φ, B=45°=Λ, …)
|
||||
LATIN_TO_GREEK = {
|
||||
"A": "Φ", "T": "Λ", "G": "Ρ", "C": "Κ",
|
||||
"B": "Ω", "S": "Σ", "P": "Π", "Z": "Ζ",
|
||||
"A": "Φ", "B": "Λ", "C": "Ρ", "G": "Κ",
|
||||
"P": "Ω", "S": "Σ", "T": "Π", "Z": "Ζ",
|
||||
}
|
||||
GREEK_TO_LATIN = {v: k for k, v in LATIN_TO_GREEK.items()}
|
||||
|
||||
|
|
@ -204,19 +208,21 @@ def decode_dna_to_bytes(sequence: str) -> bytes:
|
|||
# §4 BINARY VECTOR ENCODING: x ∈ {0,1}^n → DNA
|
||||
# ============================================================
|
||||
|
||||
def encode_binary_vector(x: List[int], bits_per_var: int = 3) -> str:
|
||||
def encode_binary_vector(x: List[int], bases_per_var: int = 3) -> str:
|
||||
"""Encode a binary vector as a Hachimoji DNA sequence.
|
||||
|
||||
Each variable gets `bits_per_var` bases (default 3 = one Hachimoji base).
|
||||
This ensures every variable has a dedicated position in the sequence.
|
||||
Each variable gets `bases_per_var` copies of A (for 0) or P (for 1).
|
||||
Redundant encoding: A has low Tm (2.0), P has high Tm (3.5), so Tm
|
||||
is monotonically proportional to the number of 1s in x.
|
||||
|
||||
Args:
|
||||
x: binary vector (list of 0s and 1s)
|
||||
bits_per_var: number of bases per variable (default 3)
|
||||
bases_per_var: number of bases per variable (default 3, for majority-vote decoding)
|
||||
|
||||
Returns:
|
||||
Hachimoji DNA string of length len(x) * bits_per_var
|
||||
Hachimoji DNA string of length len(x) * bases_per_var
|
||||
"""
|
||||
bits_per_var = bases_per_var # internal alias for callers using old parameter name
|
||||
sequence = []
|
||||
for val in x:
|
||||
# Encode each variable as a base (0 → A, 1 → P for max Tm separation)
|
||||
|
|
|
|||
|
|
@ -103,22 +103,24 @@ class TestByteEncoding(unittest.TestCase):
|
|||
self.assertEqual(decoded, b"")
|
||||
|
||||
def test_known_sequence(self):
|
||||
"""Known byte → DNA mapping."""
|
||||
"""Known byte → DNA mapping (ABCGPSTZ ordering, ASCII-sorted)."""
|
||||
# 0x00 = 00000000 → 000 000 00(pad 0) → A A A (3 bases)
|
||||
dna = encode_bytes_to_dna(b"\x00")
|
||||
self.assertEqual(dna, "AAA")
|
||||
|
||||
# 0xFF = 11111111 → 111 111 11(pad 0) → Z Z P (3 bases)
|
||||
# 0xFF = 11111111 → 111 111 11(pad 0) → Z Z T (3 bases)
|
||||
# With ABCGPSTZ: 111=7→Z, 111=7→Z, 110=6→T
|
||||
dna = encode_bytes_to_dna(b"\xff")
|
||||
self.assertEqual(dna[0], "Z") # 111
|
||||
self.assertEqual(dna[1], "Z") # 111
|
||||
self.assertEqual(dna[2], "P") # 110 (padded with 0)
|
||||
self.assertEqual(dna[0], "Z") # 111 = 7
|
||||
self.assertEqual(dna[1], "Z") # 111 = 7
|
||||
self.assertEqual(dna[2], "T") # 110 = 6 (padded with 0)
|
||||
|
||||
# 0b11010001 = 110 100 01(pad 0) = 110 100 010 → P B G
|
||||
# 0b11010001 = 110 100 01(pad 0) = 110 100 010 → T P C
|
||||
# With ABCGPSTZ: 110=6→T, 100=4→P, 010=2→C
|
||||
dna = encode_bytes_to_dna(b"\xd1")
|
||||
self.assertEqual(dna[0], "P") # 110 = 6
|
||||
self.assertEqual(dna[1], "B") # 100 = 4
|
||||
self.assertEqual(dna[2], "G") # 010 = 2
|
||||
self.assertEqual(dna[0], "T") # 110 = 6
|
||||
self.assertEqual(dna[1], "P") # 100 = 4
|
||||
self.assertEqual(dna[2], "C") # 010 = 2
|
||||
|
||||
def test_random_roundtrip(self):
|
||||
"""Random bytes roundtrip through DNA encoding."""
|
||||
|
|
@ -159,9 +161,9 @@ class TestBinaryVectorEncoding(unittest.TestCase):
|
|||
self.assertEqual(seq, "AAAPPPAAAPPP") # 0→AAA, 1→PPP, 0→AAA, 1→PPP
|
||||
|
||||
def test_single_base_per_var(self):
|
||||
"""bits_per_var=1 gives one base per variable."""
|
||||
"""bases_per_var=1 gives one base per variable."""
|
||||
x = [0, 1, 0, 1]
|
||||
seq = encode_binary_vector(x, bits_per_var=1)
|
||||
seq = encode_binary_vector(x, bases_per_var=1)
|
||||
self.assertEqual(seq, "APAP")
|
||||
|
||||
def test_roundtrip(self):
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue