diff --git a/docs/UNIFIED_THEORY.md b/docs/UNIFIED_THEORY.md index 49923253..19be9693 100644 --- a/docs/UNIFIED_THEORY.md +++ b/docs/UNIFIED_THEORY.md @@ -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` diff --git a/formal/CoreFormalism/HachimojiLUT.lean b/formal/CoreFormalism/HachimojiLUT.lean index b09053e2..683ed692 100644 --- a/formal/CoreFormalism/HachimojiLUT.lean +++ b/formal/CoreFormalism/HachimojiLUT.lean @@ -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 diff --git a/python/dna_codec.py b/python/dna_codec.py index d8776945..ffef1b73 100644 --- a/python/dna_codec.py +++ b/python/dna_codec.py @@ -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) diff --git a/tests/test_dna_codec.py b/tests/test_dna_codec.py index a54c4d3e..47162bbc 100644 --- a/tests/test_dna_codec.py +++ b/tests/test_dna_codec.py @@ -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):