FAQs + grammar v0.3.0: design archaeology from 2026-03-24 session

7 FAQ documents capturing design decisions with attribution:
- architecture.adoc — Harvard, Six Pillars, Layer model, given/traces
- type-system.adoc — Kategoria levels, why Idris2/not Agda/not ATS2, OCaml
- token-economics.adoc — Five Facets, @Budget, @neural, reversible tokens
- verification.adoc — ECHIDNA micro/full via Groove, proof caching, echidnabot
- landscape.adoc — Quasar, LMQL, DSPy, MCP, Ronacher analysis
- language-family.adoc — 007/Eclexia/Ephapax/JTV/Oblibeny convergence
- meta.adoc — VeriSimDB migration plan, attribution methodology

Each FAQ tracks: who proposed, who decided, course changes and why.
The FAQs themselves are a Layer 4 decision trace of the design process.

Grammar v0.3.0 (spec/grammar.ebnf) also in this commit:
- Sections 18-19 (token economics + Kategoria types)
- Invariants 4 (Economic) and 5 (Kategoria Harvard separation)
- Duplicate productions resolved with section cross-references

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/faq/README.adoc

@@ -0,0 +1,50 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+
+= 007 Design FAQs
+:toc: macro
+
+[.lead]
+Frequently asked questions arising from design conversations between
+Jonathan D.A. Jewell and Claude (Opus 4.6). These capture not just answers
+but *who proposed what*, *when we changed course*, and *why*.
+
+Intended to migrate to a dedicated private VeriSimDB instance for
+queryable design archaeology.
+
+toc::[]
+
+== Index
+
+[cols="1,3,1"]
+|===
+| File | Topic | Date
+
+| link:architecture.adoc[architecture.adoc]
+| Harvard Architecture, Six Pillars, Layer model
+| 2026-03-22 → 2026-03-24
+
+| link:type-system.adoc[type-system.adoc]
+| Kategoria levels, TypeLL, why Idris2 not Agda/ATS2, OCaml role
+| 2026-03-24
+
+| link:token-economics.adoc[token-economics.adoc]
+| Five Facets, @budget, @neural, speculative, cached, reversible tokens
+| 2026-03-24
+
+| link:verification.adoc[verification.adoc]
+| ECHIDNA micro/full, Groove routing, Agda as proof oracle, proof caching
+| 2026-03-24
+
+| link:landscape.adoc[landscape.adoc]
+| Quasar, LMQL, DSPy, MCP, Ronacher — what exists, what doesn't
+| 2026-03-24
+
+| link:language-family.adoc[language-family.adoc]
+| 007/Eclexia/Ephapax/JTV/Oblibeny convergence, computation-as-X thesis
+| 2026-03-24
+
+| link:meta.adoc[meta.adoc]
+| About these FAQs, VeriSimDB migration plan, decision attribution methodology
+| 2026-03-24
+|===

docs/faq/architecture.adoc

@@ -0,0 +1,105 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= Architecture FAQs
+
+== Q: What is the Harvard Architecture in 007?
+
+*Origin:* JTV (Julia-the-Viper), designed by Jewell.
+*Adopted into 007:* 2026-03-22, during genesis session.
+
+The grammar separates computation into two sublanguages:
+
+- **Data Language** — total, pure, addition-only. Guaranteed to terminate.
+  Cannot contain control flow. Evaluated deterministically by CPU.
+- **Control Language** — Turing-complete, effectful. Where agent behaviour
+  lives. Evaluated by LLM inference (costs tokens).
+
+The grammar itself prevents crossing the boundary. Agent injection is a
+parse error, not a runtime check.
+
+*Decision by:* Jewell (proposed JTV's architecture as foundation).
+Claude (identified dual role: safety + epistemological).
+
+== Q: Why does the Harvard Architecture have two roles?
+
+*Discovered:* 2026-03-22, hermeneutic dimension entry.
+*Proposed by:* Claude.
+
+1. **Safety** — prevents injection (original JTV purpose)
+2. **Epistemological** — structures the hermeneutic act by separating what
+   agents KNOW (Data) from what agents DO (Control), making interpretation
+   observable
+
+You can only study how agents interpret data if data and control are cleanly
+separated. Otherwise, interpretation and execution blur and become
+unobservable. The Harvard Architecture is the precondition for Layer 4.
+
+*Course change:* Initially seen only as a security mechanism. Reframed as
+the epistemological foundation when Layer 4 was identified.
+
+== Q: What are the six pillars?
+
+*Proposed by:* Jewell and Claude collaboratively, 2026-03-22.
+
+1. **Harvard Architecture** (JTV) — data/control separation
+2. **Actor Model** (Elixir/BEAM) — agents as supervised processes
+3. **Capability Security** (Pony/E) — compile-time permissions
+4. **Session Types** (academic PLT) — typed communication protocols
+5. **Linear Handles** (Ephapax) — no leaked or duplicated agents
+6. **Choreographic Compilation** (Chor-lambda) — global→local projection
+
+Each addresses a specific failure mode. None is individually novel; the
+synthesis is.
+
+== Q: What is the Layer model?
+
+[cols="1,2,3"]
+|===
+| Layer | Formalism | Status
+
+| 1. Grammar | EBNF | Specified (v0.3.0)
+| 2. Types | 10-layer TypeLL + Kategoria | Specified (outline)
+| 3. Operational Semantics | Small-step reduction | Specified
+| 4. Interpretive Semantics | _(Novel — no existing formalism)_ | Provisional by design
+|===
+
+*Key discovery:* `branch` is the ONLY nondeterministic construct. Layer 4
+has a small, precise surface area. Discovered while writing Layer 3 spec.
+
+*Proposed by:* Layer 4 concept — Jewell (de Man parabasis, Wittgenstein
+ladder). Layer 4 localisation to `branch` — Claude (during operational
+semantics drafting).
+
+== Q: What is the `given` clause?
+
+*Proposed by:* Jewell (Position C in telescope entry, 2026-03-22).
+
+The `given` clause declares what information is RELEVANT to a branch choice.
+Properties:
+
+- Data expressions only (Harvard-separated, cannot contain control flow)
+- May overlap between branches (shared evidence)
+- Not exhaustive (agent may consider unlisted information)
+- Part of the branch's TYPE (changing what's given changes the type)
+- Predicates are SUGGESTIONS, not guards — agent may override
+
+The agent reads the `given` and interprets. The `given` structures
+interpretation without determining it. This is de Man's parabasis — the
+ability to turn away from the suggested reading.
+
+== Q: What are decision traces?
+
+*Proposed by:* Jewell (telescope metaphor). Formalised by Claude.
+
+Every `traced` branch produces an immutable Data record:
+- Branch options available
+- `given` context for each arm
+- Which arm was chosen
+- The `trace` self-report (agent's stated reasoning)
+- Timestamp, agent ID, full hermeneutic context
+
+Traces are Data (Harvard-separated). Cannot be tampered with after creation.
+The observation must not disturb the phenomenon.
+
+*Purpose:* Not logging. Scientific instrumentation for discovering Layer 4.
+Decision traces are the raw dataset through which the structure of agent
+interpretive acts might become visible. The telescope.

docs/faq/landscape.adoc

@@ -0,0 +1,63 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= Landscape FAQs — Who Else Is Working on This?
+
+== Q: Are Quasar and LMQL "agent-first" languages?
+
+*Question by:* Jewell (2026-03-24).
+*Answer:* No. They're designed for agents as *users of tools*, not as
+*participants in a computational economy*.
+
+**Quasar** (Mell et al., arXiv 2506.12202): Agents write Python, it
+transpiles to Quasar for faster/safer execution. The agent is the *writer*,
+Quasar is the *runtime target*. No theory of what agents need — just
+pragmatic parallelism + uncertainty quantification.
+
+**LMQL** (ETH Zurich): Steers LLM *generation* with constraints. The agent
+is being *controlled*, not programming other agents. About output quality,
+not agent-to-agent interaction.
+
+Neither has session types, choreographies, Harvard separation, hermeneutic
+traces, or any theory of WHY agent computation is fundamentally different.
+They're tools for agents. 007 is a language *of* agents.
+
+== Q: What does the competitive landscape look like?
+
+*Researched by:* Claude (2026-03-24, web search).
+
+[cols="1,1,1,1,1,1,1"]
+|===
+| | Grammar | Types | Harvard | Traces | Choreo | Token Econ
+
+| Quasar | No | No | No | No | No | Parallelism
+| LMQL | Partial | Constraints | No | No | No | Constraint masking
+| DSPy | No | No | No | Logging | No | Prompt compilation
+| MCP | No | Schema | No | No | No | No
+| LangGraph | No | No | No | No | No | No
+| **007** | **Full EBNF** | **10-level** | **Core** | **Hermeneutic** | **Choreo-lambda** | **Five Facets**
+|===
+
+Nobody has the full synthesis.
+
+== Q: What did Armin Ronacher observe?
+
+*Source:* Blog post "A Language For Agents" (February 2026).
+
+Key points:
+- Agents struggle with type inference — need explicit types
+- Whitespace-based indentation is token-hostile
+- Languages in LLM training weights are easier for agents to write
+- New languages CAN succeed if designed for agent ergonomics
+
+He asked the right question without building a language. 007 answers it.
+
+== Q: Is anyone else combining formal PL design with token economics?
+
+*Searched by:* Claude (2026-03-24).
+*Result:* Nothing found.
+
+The economics literature discusses token pricing for platforms. The PL
+literature discusses resource types. Nobody appears to have connected
+them — treating inference tokens as a linear resource governed by a type
+system within a formally specified agent language.
+
+If this synthesis exists elsewhere, we haven't found it.

docs/faq/language-family.adoc

@@ -0,0 +1,69 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= Language Family FAQs
+
+== Q: How do the five languages converge?
+
+*Observed by:* Jewell (2026-03-24, "this is the aggregation of my
+thinking more generally on languages").
+*Mapped by:* Claude (Five Facets table).
+
+Each language was designed independently for a different purpose. They
+converge on one question: what is computation when agents consume it?
+
+- **007** — agents interpret, choose, trace decisions
+- **Eclexia** — computation has measurable cost (energy, time, carbon, tokens)
+- **Ephapax** — computation is physical matter (consumed once, linear)
+- **JTV** — some computation is free (total, deterministic, governed)
+- **Oblibeny** — computation is reversible (undo, reduce, minimize)
+
+Each maps to a 007 grammar construct:
+
+- 007 → `branch` / `given` / `traced`
+- Eclexia → `@budget(N)` / model-routing locales
+- Ephapax → `linear` / `@graded(N)` / `@focus(N)`
+- JTV → Data Language (free) vs Control Language (costs tokens)
+- Oblibeny → `reversible` / `cached` / `reverse`
+
+== Q: Why is 007 a standalone repo, not in nextgen-languages?
+
+*Decision by:* Jewell (2026-03-22).
+
+Privacy requirement. Other AI models (Gemini, etc.) might scrape the spec
+and generate low-quality agent swarms from a half-understood design. The
+Harvard Architecture safety guarantees need to be inextricable from the
+language before public exposure.
+
+Pointer card remains at `nextgen-languages/languages/007.md`.
+
+== Q: What is the relationship between 007 and TypeLL?
+
+TypeLL defines the 10-level type safety hierarchy. 007 implements it.
+
+007's type_expr in grammar v0.3.0 maps each TypeLL level to concrete
+syntax. TypeLL is the theory; 007 is (one) application. Kategoria is the
+research project that explores multiple routes to implementing all 10 levels.
+
+== Q: How did the son explain it?
+
+*Date:* 2026-03-24. Jewell's son summarised the project.
+
+**What he nailed (~85-90% accurate):**
+
+- Syntax can be huge because agents don't care (humans are the bottleneck)
+- De Man parabasis — same syntax, different meanings depending on context
+- LLMs read hermeneutically (lawyer/engineer/four-year-old example)
+- Type safety as the third pillar constraining the interpretive space
+- 10 acknowledged levels vs ~16 with frontier research
+- Convergence of Ephapax, Eclexia, JTV
+- "Utterly INSANE if it works"
+
+**Slight imprecisions:**
+
+- Said "Eclexia as code as matter" — Eclexia is economics, Ephapax is
+  matter (adjacent facets, easy to confuse)
+- "Tokens no longer cost anything" — overstated but directionally correct
+  for reversible + cached computation (bounded total cost, not zero)
+- TypeScript level count slightly compressed
+
+**Assessment by Claude:** "The fact that he's tracking the de Man reference
+and connecting it to type theory is genuinely impressive."

docs/faq/meta.adoc

@@ -0,0 +1,92 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= Meta FAQs — About These FAQs
+
+== Q: What is the purpose of these FAQs?
+
+Three purposes:
+
+1. **Design archaeology** — who proposed what, when we changed course, why
+   we took a different route
+2. **Layer 4 data about our own design process** — the FAQs are themselves
+   a decision trace of the human-AI collaboration that created 007
+3. **Onboarding** — if 007 ever becomes public, these explain the reasoning
+   behind non-obvious design choices
+
+== Q: How is attribution tracked?
+
+Each FAQ entry notes:
+
+- **Proposed by:** who first raised the idea (Jewell or Claude)
+- **Decision by:** who made the final call (always Jewell for design
+  decisions; Claude for mechanical implementation choices)
+- **Course change:** if we changed direction, what triggered it and when
+
+This is important because it answers the Frum question — "is the AI just
+reflecting back what the human said?" The answer is testable: if the
+attributions show genuinely different contributions (e.g., Jewell proposed
+de Man, Claude proposed Galileo's telescope — different metaphors for the
+same insight), then it's convergence, not reflection.
+
+== Q: VeriSimDB migration plan
+
+These FAQs are currently stored as AsciiDoc files in `007-lang/docs/faq/`.
+The plan is to migrate them to a dedicated private VeriSimDB instance:
+
+**Why VeriSimDB:**
+
+- Queryable — "show me all decisions where we changed course"
+- Temporal — "what did we believe about X on date Y"
+- Cross-project — can link 007 FAQs to Eclexia, Ephapax, Kategoria decisions
+- Versioned — VeriSimDB's octad model tracks changes over time
+- Machine-readable — agents can query the FAQ database programmatically
+
+**Instance plan:**
+
+[cols="1,2"]
+|===
+| Setting | Value
+
+| Repo | `hyperpolymath/design-archaeology` (private)
+| Port | TBD (check PORT-REGISTRY.md)
+| Volume | `/mnt/eclipse/verisimdb/design-archaeology`
+| Scope | All hyperpolymath design decisions (not just 007)
+| Access | Claude-only until mature (same policy as 007 itself)
+|===
+
+**Schema (tentative):**
+
+Each FAQ entry becomes a VeriSimDB octad:
+- `question` — the FAQ question
+- `answer` — the answer text
+- `proposed_by` — who raised it (human / claude / collaborative)
+- `decided_by` — who made the call
+- `date` — when
+- `project` — which project(s) this relates to
+- `superseded_by` — if this decision was later changed
+- `tags` — searchable tags (architecture, types, economics, etc.)
+
+**Timeline:** After current 007 sprint. Not urgent — the AsciiDoc files
+capture the content. VeriSimDB adds queryability and cross-project linking.
+
+== Q: What is the decision attribution methodology?
+
+When recording who proposed what:
+
+1. **"Proposed by: Jewell"** — the idea originated from the human, possibly
+   in response to a question but with substance not derivable from the question
+2. **"Proposed by: Claude"** — the idea originated from the AI, not directly
+   prompted by the human's immediate statement
+3. **"Proposed by: collaborative"** — genuinely co-created, neither party
+   could have reached it alone
+4. **"Decision by: Jewell"** — all design decisions are ultimately human
+   decisions. Claude proposes; Jewell disposes.
+5. **"Course change"** — records when a prior decision was revised, who
+   triggered the revision, and why
+
+The goal is not credit — it's *traceability*. Understanding which ideas
+came from which source helps evaluate the quality of human-AI collaboration
+and may reveal patterns about when each party contributes most effectively.
+
+This is itself a Layer 4 question: the FAQs are a decision trace of the
+design process, and analysing the attribution patterns is a form of
+hermeneutic analysis of that trace.