# 0-Core-Formalism

**Purpose:** Formal foundations for the entire Research Stack — Lean modules, bind primitive, Triumvirate consensus, core source.

**No external dependencies.** All other layers depend on this.

## Contents (Target)

| Source | Destination |
|--------|-------------|
| `0-Core-Formalism/lean/Semantics/` | `0-Core-Formalism/lean/Semantics/` |
| `core/` | `0-Core-Formalism/core/` |

## Concepts

- **bind** — State → (State → Action) → State
- **TriumvirateClock** — ternary consensus (ADD/PAUSE/SUBTRACT)
- **Builder/Judge/Warden** — roles mapped to hardware registers
- **OTOM** — Ordered Transformation & Orchestration Model

## Build

```bash
cd "0-Core-Formalism/lean/Semantics"
lake build
```

**Current baseline:** `lake build` reports **3314 jobs, 0 errors**.

## Recent Additions

Recently added/blessed Lean/Semantics modules:

- `Semantics.SDPVerify`
- `Semantics.GoormaghtighCert`
- `Semantics.HachimojiManifoldAxiom` / `Semantics.HachimojiSubstitution`
- `Semantics.GeneticBraidBridge`
- `Semantics.SieveLemmas`
- `Semantics.InteractionGraphSidon`

## Fixed-Point Constraint

Core compute paths use `Q16_16` fixed-point arithmetic. `Float` is not allowed in compute paths; `ofFloat` is only permitted at the external boundary (JSON parsing, sensor input) and must be immediately bracketed to `Q16_16`.

## Dependency Graph / Mathblob Insight

The dependency graph and Gremlin mathblob work serve as documentation and insight tooling for surfacing module relationships and formal-structure context within the Semantics surface.