diff --git a/.gitea/workflows/verify.yaml b/.gitea/workflows/verify.yaml
new file mode 100644
index 0000000..cab084e
--- /dev/null
+++ b/.gitea/workflows/verify.yaml
@@ -0,0 +1,13 @@
+name: Verify syntax DAG
+on: [push, pull_request]
+jobs:
+  verify:
+    runs-on: ubuntu24.04-x64-lean4.35
+    steps:
+      - uses: https://github.com/actions/checkout@v4
+      - name: Install wheels in an isolated environment
+        run: |
+          python3 -m venv .venv
+          .venv/bin/python -m pip install --only-binary=:all: -r requirements.txt
+      - name: Verify graph commits and decoding
+        run: .venv/bin/python -m unittest -v
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..a230a78
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+.venv/
+__pycache__/
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..474cec3
--- /dev/null
+++ b/README.md
@@ -0,0 +1,36 @@
+# Syntax DAG Transformer
+
+An English-language prototype that combines spaCy's tokenizer and learned
+dependency parser with explicit graph rules. The graph interface can support
+other encoders and relation miners as the prototype evolves.
+
+```text
+The road flooded because it rained.
+  → Cause: it rained. Effect: The road flooded.
+```
+
+Run with Python 3.12 after installing `requirements.txt`.
+
+```sh
+python -m syntax_dag --commit 'The road flooded because it rained.'
+python -m unittest -v
+```
+
+Omit `--commit` to recover the original token surfaces and whitespace. The
+command prints one final newline.
+
+1. `Encoder` creates token nodes with original whitespace and head-to-dependent
+   edges. The causal rule adds clause nodes with edges to their member tokens.
+   A token can have incoming edges from both a clause and a syntactic head.
+2. The rule mines a candidate `cause → effect` edge with provenance from a
+   trailing `because` clause. The candidate stays separate until committed.
+3. `SyntaxDAG.commit` creates a new immutable graph revision and records the
+   proposal. A cycle rejects the entire edit. Repeating a commit on the same
+   revision returns that revision.
+4. `Decoder` uses committed causal edges to select the clause order and labels.
+   Text outside the selected clauses retains its original surface form.
+
+The first rule covers simple affirmative past-tense statements with a trailing
+finite causal clause. Extraction is heuristic and depends on parser accuracy.
+Commits are in-memory graph edits. The prototype uses explicit authorization
+via the CLI flag and has no learned rewrite policy.
diff --git a/requirements.txt b/requirements.txt
new file mode 100644
index 0000000..27a1369
--- /dev/null
+++ b/requirements.txt
@@ -0,0 +1,2 @@
+spacy==3.8.11
+en-core-web-sm @ https://github.com/explosion/spacy-models/releases/download/en_core_web_sm-3.8.0/en_core_web_sm-3.8.0-py3-none-any.whl
diff --git a/syntax_dag.py b/syntax_dag.py
new file mode 100644
index 0000000..6586703
--- /dev/null
+++ b/syntax_dag.py
@@ -0,0 +1,164 @@
+"""Encode English text, commit supported graph edits, and decode a revision."""
+
+import argparse
+from dataclasses import dataclass, replace
+from graphlib import TopologicalSorter
+
+import spacy
+
+
+@dataclass(frozen=True)
+class Token:
+    text: str
+    whitespace: str
+
+
+@dataclass(frozen=True)
+class Clause:
+    id: int
+    start: int
+    stop: int
+
+
+@dataclass(frozen=True)
+class Edge:
+    source: int
+    target: int
+    kind: str
+
+
+@dataclass(frozen=True)
+class Proposal:
+    edge: Edge
+    marker: int
+    rule: str
+
+
+@dataclass(frozen=True)
+class SyntaxDAG:
+    tokens: tuple[Token, ...]
+    clauses: tuple[Clause, ...]
+    edges: tuple[Edge, ...]
+    proposals: tuple[Proposal, ...]
+    history: tuple[Proposal, ...] = ()
+
+    def __post_init__(self):
+        nodes = set(range(len(self.tokens))) | {clause.id for clause in self.clauses}
+        sorter = TopologicalSorter()
+        for node in nodes:
+            sorter.add(node)
+        for edge in self.edges:
+            if edge.source not in nodes or edge.target not in nodes:
+                raise ValueError("Edge endpoint is missing")
+            sorter.add(edge.target, edge.source)
+        tuple(sorter.static_order())
+
+    def commit(self, proposal: Proposal):
+        if proposal not in self.proposals:
+            raise ValueError("Proposal was not mined from this graph")
+        if proposal in self.history:
+            return self
+        return replace(
+            self,
+            edges=(*self.edges, proposal.edge),
+            history=(*self.history, proposal),
+        )
+
+
+class Encoder:
+    def __init__(self):
+        self.nlp = spacy.load("en_core_web_sm", disable=["ner"])
+
+    def encode(self, text: str) -> SyntaxDAG:
+        doc = self.nlp(text)
+        tokens = tuple(Token(token.text, token.whitespace_) for token in doc)
+        edges = [
+            Edge(token.head.i, token.i, token.dep_)
+            for token in doc
+            if token.head != token
+        ]
+        clauses = []
+        proposals = []
+        for sentence in doc.sents:
+            match = self._causal_marker(sentence)
+            if match is None:
+                continue
+            marker, end = match
+            effect = Clause(len(tokens) + len(clauses), sentence.start, marker.i)
+            cause = Clause(effect.id + 1, marker.i + 1, end)
+            clauses.extend((effect, cause))
+            for clause in (effect, cause):
+                edges.extend(
+                    Edge(clause.id, index, "contains")
+                    for index in range(clause.start, clause.stop)
+                )
+            proposals.append(Proposal(Edge(cause.id, effect.id, "causes"),
+                                      marker.i, "trailing-because"))
+        return SyntaxDAG(tokens, tuple(clauses), tuple(edges), tuple(proposals))
+
+    @staticmethod
+    def _causal_marker(sentence):
+        markers = [token for token in sentence if token.lower_ == "because"]
+        if len(markers) != 1 or sentence[-1].text != ".":
+            return None
+        marker = markers[0]
+        verb = marker.head
+        end = sentence.end - 1
+        if (
+            marker.dep_ != "mark"
+            or verb.dep_ != "advcl"
+            or verb.head != sentence.root
+            or not sentence.start <= sentence.root.i < marker.i
+            or not marker.i < verb.i < end
+            or sentence.root.pos_ != "VERB"
+            or verb.pos_ != "VERB"
+            or sentence.root.tag_ != "VBD"
+            or verb.tag_ != "VBD"
+            or any(token.is_punct or token.is_space for token in sentence[:-1])
+            or any(token.dep_ in {"neg", "aux", "conj"} for token in sentence)
+            or not any(child.dep_ == "nsubj" for child in sentence.root.children)
+            or not any(child.dep_ == "nsubj" for child in verb.children)
+            or {token.i for token in verb.subtree} != set(range(marker.i, end))
+        ):
+            return None
+        return marker, end
+
+
+class Decoder:
+    def decode(self, graph: SyntaxDAG) -> str:
+        clauses = {clause.id: clause for clause in graph.clauses}
+        edits = {}
+        for edge in graph.edges:
+            if edge.kind != "causes":
+                continue
+            cause, effect = clauses[edge.source], clauses[edge.target]
+            cause_text = self._surface(graph, cause.start, cause.stop).rstrip()
+            effect_text = self._surface(graph, effect.start, effect.stop).rstrip()
+            edits[effect.start] = (cause.stop, f"Cause: {cause_text}. Effect: {effect_text}")
+        output = []
+        index = 0
+        while index < len(graph.tokens):
+            stop, surface = edits.get(index, (index + 1, self._surface(graph, index, index + 1)))
+            output.append(surface)
+            index = stop
+        return "".join(output)
+
+    @staticmethod
+    def _surface(graph, start, stop):
+        return "".join(token.text + token.whitespace for token in graph.tokens[start:stop])
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("text")
+    parser.add_argument("--commit", action="store_true", help="Apply mined causal edits")
+    args = parser.parse_args()
+    graph = Encoder().encode(args.text)
+    if args.commit:
+        for proposal in graph.proposals:
+            graph = graph.commit(proposal)
+    print(Decoder().decode(graph))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/test_syntax_dag.py b/test_syntax_dag.py
new file mode 100644
index 0000000..499a8d5
--- /dev/null
+++ b/test_syntax_dag.py
@@ -0,0 +1,54 @@
+import unittest
+from dataclasses import replace
+from graphlib import CycleError
+
+from syntax_dag import Decoder, Edge, Encoder, Proposal
+
+
+class SyntaxDAGTest(unittest.TestCase):
+    @classmethod
+    def setUpClass(cls):
+        cls.encoder = Encoder()
+        cls.decoder = Decoder()
+
+    def test_round_trip(self):
+        for text in ("", "  \t", "  It rained.\n\nThe road flooded.  "):
+            with self.subTest(text=text):
+                graph = self.encoder.encode(text)
+                self.assertEqual(self.decoder.decode(graph), text)
+                self.assertFalse(graph.proposals)
+
+    def test_causal_commit(self):
+        text = "The road flooded because it rained.  They waited."
+        graph = self.encoder.encode(text)
+        proposal, = graph.proposals
+        self.assertTrue(any(
+            len({edge.source for edge in graph.edges if edge.target == node}) > 1
+            for node in range(len(graph.tokens))
+        ))
+        committed = graph.commit(proposal)
+        self.assertEqual(self.decoder.decode(graph), text)
+        self.assertEqual(
+            self.decoder.decode(committed),
+            "Cause: it rained. Effect: The road flooded.  They waited.",
+        )
+        self.assertEqual(committed.history, (proposal,))
+        self.assertIs(committed.commit(proposal), committed)
+        self.assertNotIn(proposal.edge, graph.edges)
+
+    def test_cycle_rejects_entire_commit(self):
+        graph = self.encoder.encode("The road flooded because it rained.")
+        original, = graph.proposals
+        reverse = Proposal(Edge(original.edge.target, original.edge.source, "causes"),
+                           original.marker, "test")
+        committed = replace(graph.commit(original), proposals=(original, reverse))
+        with self.assertRaises(CycleError):
+            committed.commit(reverse)
+        self.assertEqual(committed.history, (original,))
+        self.assertNotIn(reverse.edge, committed.edges)
+
+    def test_negation_and_questions_are_left_alone(self):
+        for text in ("The road did not flood because it rained.",
+                     "Did the road flood because it rained?"):
+            with self.subTest(text=text):
+                self.assertFalse(self.encoder.encode(text).proposals)