mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-18 13:40:33 +00:00
allaun
cd0860e3ae
New files:
- docs/reviews/avmisa_audit_report.md: Full AVMIsa rigidity & vulnerability audit
(8 surfaces found, 5 mitigated, 2 open)
- formal/BindingSite/BindingSiteTypes.lean: Binding site type definitions
- formal/CoreFormalism/GoormaghtighEnumeration.lean: Goormaghtigh conjecture enumeration
- formal/SilverSight/HachimojiCharClass.lean: Hachimoji character classification
- formal/SilverSight/HachimojiN8.lean: N=8 minimal alphabet theorem
- formal/SilverSight/HachimojiN8Bridge.lean: Bridge between HachimojiCharClass and N8
- formal/SilverSight/PhiConsistency.lean: Phi pipeline consistency checks
- formal/SilverSight/PhiDNALayout.lean: DNA layout for Phi-encoded equations
- formal/SilverSight/PhiPipelineReceipt.lean: Receipt format for Phi pipeline
157 lines
6 KiB
Text
157 lines
6 KiB
Text
/-
|
||
PhiDNALayout.lean — Ring 3: 30-base layout type with window invariants
|
||
|
||
phi.embed.encode_phi builds a 30-base hachimoji DNA sequence in four layers:
|
||
|
||
bases 0-7 : F(E) — byte-class histogram (first 8 of 12 classes)
|
||
bases 8-15 : τ(E) — AST node-type histogram (first 8 of 18 NODE_TYPES)
|
||
bases 16-23 : δ(E) — child-ordering histogram (first 8 δ values)
|
||
bases 24-29 : 6 consistency rules (G = pass, T = fail ONLY)
|
||
|
||
Source (phi.embed.py lines 135-143):
|
||
F_dna = _vec_to_bases(F[:8])
|
||
tau_dna = _vec_to_bases(tau[:8] ...)
|
||
delta_dna = _vec_to_bases((delta + [0.5]*8)[:8] ...)
|
||
consistency_dna = "".join("G" if ... else "T" for r in RULE_ORDER)
|
||
full_sequence = F_dna + tau_dna + delta_dna + consistency_dna -- len 30
|
||
|
||
The key structural invariant: bases 24-29 are BINARY (only G or T).
|
||
Layers 1-3 are unrestricted (any of the 8 HachimojiBase constructors).
|
||
|
||
Anti-drift role: Ring 3 wire in the outward dependency spiral.
|
||
Any change to the 8+8+8+6 partition, or to Layer 4's binary encoding,
|
||
breaks this bridge before Ring 4 (the 6 consistency rules).
|
||
-/
|
||
|
||
import SilverSight.HachimojiCharClass
|
||
import Mathlib.Tactic
|
||
|
||
namespace SilverSight.PhiDNALayout
|
||
|
||
open HachimojiBase
|
||
open SilverSight.HachimojiCharClass
|
||
|
||
-- ============================================================
|
||
-- §1 LAYOUT CONSTANTS
|
||
-- ============================================================
|
||
|
||
/-- Total bases in a Φ-encoded DNA sequence. -/
|
||
def DNA_LEN : ℕ := 30
|
||
|
||
/-- Each of layers 1-3 has 8 bases. -/
|
||
def LAYER_WIDTH : ℕ := 8
|
||
|
||
/-- Layer 4 has exactly 6 bases (one per consistency rule). -/
|
||
def CONSISTENCY_WIDTH : ℕ := 6
|
||
|
||
theorem layout_sum : 3 * LAYER_WIDTH + CONSISTENCY_WIDTH = DNA_LEN := by decide
|
||
|
||
-- ============================================================
|
||
-- §2 LAYOUT TYPE
|
||
-- ============================================================
|
||
|
||
/-- A valid Φ-encoded DNA sequence.
|
||
The only structural invariant is Layer 4: bases 24-29 are binary
|
||
(G = rule passed, T = rule failed). Layers 1-3 are unrestricted. -/
|
||
structure PhiLayout where
|
||
seq : Fin 30 → HachimojiBase
|
||
h_layer4 : ∀ i : Fin 6,
|
||
seq ⟨24 + i.val, by omega⟩ = G ∨
|
||
seq ⟨24 + i.val, by omega⟩ = T
|
||
|
||
-- ============================================================
|
||
-- §3 WINDOW SELECTORS
|
||
-- ============================================================
|
||
|
||
/-- Layer 1: F(E) byte-class frequencies (bases 0-7). -/
|
||
def PhiLayout.layer1 (d : PhiLayout) : Fin 8 → HachimojiBase :=
|
||
fun i => d.seq ⟨i.val, by omega⟩
|
||
|
||
/-- Layer 2: τ(E) AST node-type frequencies (bases 8-15). -/
|
||
def PhiLayout.layer2 (d : PhiLayout) : Fin 8 → HachimojiBase :=
|
||
fun i => d.seq ⟨8 + i.val, by omega⟩
|
||
|
||
/-- Layer 3: δ(E) child-ordering frequencies (bases 16-23). -/
|
||
def PhiLayout.layer3 (d : PhiLayout) : Fin 8 → HachimojiBase :=
|
||
fun i => d.seq ⟨16 + i.val, by omega⟩
|
||
|
||
/-- Layer 4: consistency rule pass/fail (bases 24-29). -/
|
||
def PhiLayout.layer4 (d : PhiLayout) : Fin 6 → HachimojiBase :=
|
||
fun i => d.seq ⟨24 + i.val, by omega⟩
|
||
|
||
-- ============================================================
|
||
-- §4 PARTITION LEMMAS
|
||
-- ============================================================
|
||
|
||
/-- Every DNA position belongs to exactly one layer. -/
|
||
theorem layer_partition (i : Fin 30) :
|
||
i.val < 8 ∨ (8 ≤ i.val ∧ i.val < 16) ∨
|
||
(16 ≤ i.val ∧ i.val < 24) ∨ (24 ≤ i.val) := by omega
|
||
|
||
/-- Layer selectors correspond to the right slice of seq. -/
|
||
@[simp] theorem layer1_val (d : PhiLayout) (i : Fin 8) :
|
||
d.layer1 i = d.seq ⟨i.val, by omega⟩ := rfl
|
||
|
||
@[simp] theorem layer2_val (d : PhiLayout) (i : Fin 8) :
|
||
d.layer2 i = d.seq ⟨8 + i.val, by omega⟩ := rfl
|
||
|
||
@[simp] theorem layer3_val (d : PhiLayout) (i : Fin 8) :
|
||
d.layer3 i = d.seq ⟨16 + i.val, by omega⟩ := rfl
|
||
|
||
@[simp] theorem layer4_val (d : PhiLayout) (i : Fin 6) :
|
||
d.layer4 i = d.seq ⟨24 + i.val, by omega⟩ := rfl
|
||
|
||
-- ============================================================
|
||
-- §5 LAYER 4 BINARY CONSTRAINT
|
||
-- ============================================================
|
||
|
||
/-- Layer 4 bases are binary: only G (pass) or T (fail). -/
|
||
theorem layer4_binary (d : PhiLayout) (i : Fin 6) :
|
||
d.layer4 i = G ∨ d.layer4 i = T := d.h_layer4 i
|
||
|
||
/-- Layer 4 never contains A, B, C, P, S, or Z. -/
|
||
theorem layer4_not_ABCPSZ (d : PhiLayout) (i : Fin 6) :
|
||
d.layer4 i ≠ A ∧ d.layer4 i ≠ B ∧ d.layer4 i ≠ C ∧
|
||
d.layer4 i ≠ P ∧ d.layer4 i ≠ S ∧ d.layer4 i ≠ Z := by
|
||
obtain (h | h) := layer4_binary d i <;> rw [h] <;> decide
|
||
|
||
-- ============================================================
|
||
-- §6 CONNECTION TO RING 2 (CharClass)
|
||
-- ============================================================
|
||
|
||
/-- The char class encoded at Layer 1 slot i. -/
|
||
def layer1CharClass (d : PhiLayout) (i : Fin 8) : PhiCharClass :=
|
||
baseToCharClass (d.layer1 i)
|
||
|
||
/-- Roundtrip: the HachimojiBase at slot i is the base for char class i. -/
|
||
theorem layer1_charclass_roundtrip (d : PhiLayout) (i : Fin 8) :
|
||
charClassToBase (layer1CharClass d i) = d.layer1 i :=
|
||
base_charclass_roundtrip (d.layer1 i)
|
||
|
||
-- ============================================================
|
||
-- §7 SIMPLE CONSTRUCTOR (for witnesses)
|
||
-- ============================================================
|
||
|
||
/-- Build a PhiLayout from four function arguments.
|
||
Layer 4: con i = true → G (pass), false → T (fail). -/
|
||
def mkPhiLayout
|
||
(f : Fin 8 → HachimojiBase)
|
||
(tau : Fin 8 → HachimojiBase)
|
||
(del : Fin 8 → HachimojiBase)
|
||
(con : Fin 6 → Bool) : PhiLayout where
|
||
seq := fun ⟨n, hn⟩ =>
|
||
if h1 : n < 8 then f ⟨n, h1⟩
|
||
else if h2 : n < 16 then tau ⟨n - 8, by omega⟩
|
||
else if h3 : n < 24 then del ⟨n - 16, by omega⟩
|
||
else if con ⟨n - 24, by omega⟩ then G else T
|
||
h_layer4 := by
|
||
intro ⟨j, hj⟩
|
||
have h1 : ¬(24 + j < 8) := by omega
|
||
have h2 : ¬(24 + j < 16) := by omega
|
||
have h3 : ¬(24 + j < 24) := by omega
|
||
simp only [dif_neg h1, dif_neg h2, dif_neg h3]
|
||
split_ifs with _h
|
||
· exact Or.inl rfl
|
||
· exact Or.inr rfl
|
||
|
||
end SilverSight.PhiDNALayout
|