mirror of
https://github.com/allaunthefox/BioSight.git
synced 2026-07-30 18:56:17 +00:00
allaun
6f36ec42e7
python/phi/test_verified_units.py (V4 Critical mitigation):
- Add _ediv() implementing Euclidean division matching Lean 4 Int.div
(remainder always >= 0; matches Python // for positive divisors only)
- q16_mul uses // directly (divisor 65536 always positive)
- q16_div uses _ediv() for correct handling of negative divisors
- q16_div returns 2147483647 sentinel on division by zero
- Document int_sqrt floor-division rationale (non-negative operands)
- Verified: 6/6 edge cases match Lean
AGENTS.md:
- Add anti-drift multi-pass (Python -> Lean -> RRC -> Research Stack)
- Add N=8 root dependency on SilverSight HachimojiN8 theorem
- Add tau/delta mirror rule for gate formalization priority
- Clarify BioSight as domain instance, not independent decision maker
- Clarify Research Stack as read-only regression oracle
.gitignore:
- Add freellmapi-setup/
113 lines
4.6 KiB
Markdown
113 lines
4.6 KiB
Markdown
# 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
|
||
|
||
```bash
|
||
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.
|