BioSight/AGENTS.md

BioSight — Equation-to-DNA Φ Encoding Pipeline

Status: Active, v0.1.0

BioSight encodes mathematical equations as hachimoji DNA sequences for Adleman/Lipton-style DNA computing. The Φ mapping has 4 layers:

1. F(E) — byte-class histogram over Δ₇ (8 character classes)
2. Phase alphabet — implicit in the mapping from Δ₇ to bases
3. τ(E) + δ(E) — parse tree structure (node types + child ordering)
4. Consistency — 6 rules → allele-specific PCR G/T pass/fail

Ground Rules

• Decision logic is in Lean — BioSight shims are Python I/O only. Any Python path making an admissibility or routing decision without a SilverSight receipt is drift. File it immediately as a pending SilverSight gate.
• No floats in compute paths — phi.charclass and phi.embed use integer arithmetic for all core encoding. Only phi.output uses math.acos (for Fisher distance in Adleman graph building).
• Pure functions — every phi module is a pure function of its equation string input. No state, no I/O, no side effects.
• Reproducibility — two invocations on the same equation must produce identical DNA sequences (deterministic byte-class and AST order).
• Rotation trigger — any time phi.consistency makes an ADMIT/QUARANTINE call, check whether a SilverSight receipt backs it. If not, that check is the next SilverSight gate to formalize.
• τ/δ mirror rule — the Lean proof structure for any gate must mirror BioSight's τ (topology) and δ (depth) values for that equation. High δ → WF-recursive Lean definitions. High τ diversity → wider typeclass hierarchy in SilverSight.

Anti-Drift Multi-Pass

Every decision — no matter how minor — must survive all four passes:

Pass	Layer	Authority
1	Python (phi.*)	I/O encoding only — no decisions
2	Lean (SilverSight gate)	Formal authority — closes the decision
3	RRC pipeline (rigour_pipeline.py)	Cross-repo alignment
4	Research Stack (~/Research Stack, read-only)	Regression oracle

Session start: run python3 -m py_compile phi/*.py equation_dna_encoder.py and confirm phi.encode is deterministic before any new encoding work.

N=8 Root Dependency

BioSight's entire 8-base alphabet choice depends on the SilverSight theorem:

N = 8 = min { N : Nyquist(N) ∧ Q16_16(N) ∧ DNA-subset(N) }

Target: formal/SilverSight/HachimojiN8.lean in the SilverSight repo. Until that theorem is closed with zero sorrys, the alphabet choice is documented justification only, not formal proof.

Core Modules

Module	Layer	Responsibility
phi.charclass	1	8-class byte histogram → F(E) ∈ Δ₇
phi.ast_parse	3	Python AST → τ(E) + δ(E) distributions
phi.consistency	4	6 rules → ADMIT/QUARANTINE
phi.embed	Core	(F, τ, δ) → 30-base hachimoji DNA
phi.output	Formats	FASTQ, Adleman graph, PCR protocol

DNA Layout (30 bases)

bases  0-7:   F(E) — byte-class frequencies on Δ₇
bases  8-15:  τ(E) — parse tree node-type frequencies
bases 16-23:  δ(E) — child-ordering frequencies
bases 24-29:  Layer 4 consistency (G=pass, T=fail)

External Integration

• BioComputing (https://github.com/Abesuden/BioComputing, MIT): Our phi.output.to_adleman_graph() builds vertices+edges that feed directly into hampath.connectNodes() and sattv.createNodes(). Clone it alongside BioSight for wet-lab DNA sequence generation.

Key References

• Adleman (1994) Science 266:1021–1024 — 7-vertex Hamiltonian path
• Lipton (1995) Science 268:542–545 — SAT generalization
• Hoshika et al. (2019) Science 363:884–887 — 8-base hachimoji alphabet
• Newton et al. (1989) Nucleic Acids Res 17:2503 — allele-specific PCR

Build & Test

cd python
python3 -m py_compile phi/*.py equation_dna_encoder.py
python3 -c "import phi; print(phi.encode_phi('x + 1 = 2'))"

SilverSight Relationship

BioSight is the first domain instance of the SilverSight framework. SilverSight (/home/allaun/SilverSight) owns all formal Lean logic.

• BioSight imports SilverSight receipts; it never contains formal proofs.
• BioSight feeds (τ, δ) distributions back to SilverSight as the work queue for new gates (high-δ equations → WF-recursive gate; high-τ → wider typeclass).
• If BioSight needs a new theorem or receipt, open a pending gate entry in dag/graph.md and implement the gate in formal/SilverSight/ first.
• ~/Research\ Stack is read-only archive — consult it only as a regression oracle; never reference it as an active dependency.