diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1d825ed..322ae30 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,18 +8,36 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ### Added
-- Comprehensive enterprise-level documentation structure
-- AGPLv3 license for strong copyleft protection
-- Complete contribution guidelines with Fatima Test emphasis
-- Security policy for vulnerability reporting
-- Code of conduct emphasizing language inclusivity
-- Enhanced .gitignore for comprehensive coverage
+- Gradle wrapper, so `./gradlew build` works from a fresh clone
+- CI workflow: grammar build (ANTLR warnings are errors), tests, example parsing
+- Documentation test: every ```mpl code block in README, spec and whitepaper must parse
+- Canonical call syntax `f(a, b)` with nullary calls `f()`
+- Wired-in operators: `≜` definition, `⊕`/`⊖` postfix resources, `⇀_ch`/`↽_ch` channels, `‧` module access, unary minus, `/` as ASCII alias of `÷`
+- DECISIONS.md recording each design resolution with rejected alternatives
 
 ### Changed
+- One canonical form per construct: guarded alternatives `(c ⟹ r) | fallback`, `✎` output, `↯pattern ⟹ expr` handler clauses, exactly one ASCII escape per glyph
+- `;` has a single role (sequence separator, trailing permitted)
+- Identifiers may no longer start with `_`, so subscripts lex correctly
+- precedence.csv and glyph-escapes.md regenerated to match the grammar exactly
+- README claims reduced to what CI verifies
+- Comprehensive enterprise-level documentation structure
+- AGPLv3 license for strong copyleft protection (changed from MIT)
 - README transformed into moonshot vision document emphasizing cognitive justice
-- License changed from MIT to AGPLv3 for community protection
 - Whitepaper updated to v2.0 with educational narrative focus
 
+### Fixed
+- Grammar compiles: removed mutual left recursion (errors 119/148) and shadowed tokens (warning 184)
+- Generated parser package no longer declared twice
+- Gradle finds the grammar (src/main/antlr4) and the ParseExamples main class
+- Test harness uses CharStreams; supplementary-plane glyphs (𝔹, 𝓜, 🖫) now tokenize
+- Examples 03 and 05 parse (canonical handler arrow; real placeholder body)
+
+### Removed
+- Dead tokens with no parser rule: `?` (QUERY), `∃`, `⇐`, `→`, `.`
+- Juxtaposition function application (`f x`)
+- C-style ternary and `📤` from all documentation
+
 ## [2.0.0] - 2025-01-26
 
 ### Added
diff --git a/DECISIONS.md b/DECISIONS.md
index 15a649e..9049bd1 100644
--- a/DECISIONS.md
+++ b/DECISIONS.md
@@ -27,3 +27,6 @@ against the existing examples.
 - **Exactly one ASCII escape per glyph** (`\lambda` not `\lam`, `\leftarrow` not `\gets`, `\neq` not `\ne`, `\nat` not `\N`, …); rejected: alias sets (two ways to write the same token).
 - **`%` (modulo), `∑`, `√`, `²`, `|x|`, ranges `[a..b]`, indexing/slicing, `where`, and record field access are NOT in M0** — every document says so instead of using them; deferred to M1 with semantics, not smuggled in via prose.
 - **Lambda parameters are a bare comma-separated pattern list** (`λa, b: body`); rejected: parenthesized parameter lists `λ(a, b):` (two ways to write parameters).
+- **`‧` gets the escape `\middot`** so the "every glyph has an ASCII escape" claim stays true; rejected: leaving MIDDOT as the one escape-less glyph.
+- **`glyph-escapes.md` and `precedence.csv` are the only symbol/precedence tables**; the whitepaper appendix points at them instead of duplicating them; rejected: parallel tables that drift (the old appendix disagreed with the lexer on several code points and escapes).
+- **Documentation code blocks are fenced ```mpl only if they parse today**; M1+ sketches are fenced as plain text with an explicit "not yet parseable" caption, and a CI test enforces the rule for README, spec, and whitepaper.
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 369a4e0..696ea69 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -2,6 +2,11 @@
 
 This document describes the high-level architecture of the Mathematical Programming Language (MPL) implementation.
 
+**Status**: only the lexing and parsing layers exist today (see the README's
+project status). Everything from semantic analysis down — and the runtime,
+error-message, performance and security sections below — describes the
+*target* architecture, not shipped code.
+
 ## Overview
 
 MPL is designed as a multi-layer system that transforms mathematical notation into executable code:
@@ -60,22 +65,22 @@ MPL is designed as a multi-layer system that transforms mathematical notation in
 ### 1. Grammar Definition (`src/main/antlr4/MPL.g4`)
 
 The heart of MPL is its ANTLR 4 grammar that defines:
-- **70+ Mathematical Operators**: From basic arithmetic to advanced calculus
+- **Mathematical Operators**: every glyph with exactly one meaning and one ASCII escape ([glyph-escapes.md](../glyph-escapes.md))
 - **Effect Operators**: Exception handling (↯/↴), concurrency (‖), resources (⊕/⊖)
-- **Precedence Rules**: Mathematically consistent operator precedence
-- **Zero Conflicts**: No shift/reduce or reduce/reduce conflicts
+- **Precedence Rules**: a documented chain ([precedence.csv](../precedence.csv))
+- **CI-clean**: compiles with zero ANTLR errors and warnings (`-Werror`)
 
-Key grammar features:
+Key grammar rules (excerpted from the real grammar):
 ```antlr
-// Example: Function definition
-functionDef : name=IDENTIFIER '≜' lambda ;
-lambda      : 'λ' params ':' expression ;
+// Definition and assignment levels of the precedence chain
+defExpr    : assignExpr (DEFINITION defExpr)? ;      // x ≜ e
+assignExpr : condExpr (LEFTARROW assignExpr)? ;      // x ← e
 
-// Example: Mathematical operations
-expression  : expression '×' expression    # Multiplication
-            | expression '÷' expression    # Division
-            | '∑' '(' var '∈' range ':' expression ')' # Summation
-            ;
+// Guarded alternatives: (condition ⟹ result) | fallback
+condExpr   : impliesExpr (BAR impliesExpr)* ;
+
+// λx: body, λx,y: body, λx∈ℝ: body
+lambda     : LAMBDA_VAR pattern (IN condExpr)? COLON expr ;
 ```
 
 ### 2. Symbol System
@@ -83,21 +88,20 @@ expression  : expression '×' expression    # Multiplication
 MPL uses a three-tier symbol system:
 
 1. **Unicode Symbols** (Primary)
-   - Direct mathematical notation: ∀, ∃, λ, ∑, ∏
+   - Direct mathematical notation: ∀, λ, ∈, ⟹
    - Effect operators: ↯, ↴, ‖, ⇀, ↽
-   - Type symbols: ℕ, ℤ, ℝ, ℂ, 𝔹
+   - Type symbols: ℕ, ℤ, ℚ, ℝ, ℂ, 𝔹
 
 2. **ASCII Escapes** (Fallback)
-   - Every symbol has an escape: `\forall`, `\lambda`, `\sum`
-   - Bidirectional conversion supported
-   - Defined in `glyph-escapes.md`
+   - Every symbol has exactly one escape: `\forall`, `\lambda`, …
+   - Defined in `glyph-escapes.md` (kept in lockstep with the lexer)
 
 3. **Multi-Modal Input** (Future)
    - Voice recognition for mathematical terms
    - Visual palette selection
    - Handwriting recognition
 
-### 3. Type System
+### 3. Type System (planned, M1)
 
 MPL features a hybrid type system:
 
@@ -146,7 +150,7 @@ MPLVisitor visitor = new MPLASTBuilder();
 AST ast = visitor.visit(tree);
 ```
 
-### 6. Runtime Architecture
+### 6. Runtime Architecture (planned)
 
 The MPL runtime provides:
 
@@ -180,43 +184,43 @@ The MPL runtime provides:
 3. AST construction
 4. Syntax error recovery
 
-### Phase 3: Semantic Analysis
+### Phase 3: Semantic Analysis (planned)
 1. Symbol table construction
 2. Type inference
 3. Effect analysis
 4. Semantic error checking
 
-### Phase 4: Optimization
+### Phase 4: Optimization (planned)
 1. Constant folding
 2. Common subexpression elimination
 3. Parallelism detection
 4. Effect optimization
 
-### Phase 5: Code Generation
+### Phase 5: Code Generation (planned)
 Options for different targets:
 - **JVM Bytecode**: For Java interoperability
 - **LLVM IR**: For native compilation
 - **JavaScript**: For web execution
 - **Python**: For educational use
 
-## Error Handling
+## Error Handling (planned)
 
-MPL provides comprehensive error messages with:
+Today the parser emits standard ANTLR diagnostics. The goal is comprehensive error messages with:
 1. **Unicode-aware positioning**: Correct column numbers for multi-byte characters
 2. **Multi-language messages**: Errors in user's native language
 3. **Visual error display**: Highlighting problematic symbols
 4. **Suggestion system**: Common fixes for typical mistakes
 
-Example error:
+Envisioned example error:
 ```
-Error at line 3, column 15:
-  ∑(i ∈ [1,10] : i²²)
-                  ^^
-  Syntax error: Unexpected ² after ²
-  Did you mean: i² × ²  or  i⁴?
+Error at line 3, column 12:
+  (x > 0 ⟹ x | -x
+             ^
+  Syntax error: missing ')' before '|'
+  Guarded alternatives read: (condition ⟹ result) | fallback
 ```
 
-## Performance Considerations
+## Performance Considerations (planned)
 
 1. **Parser Performance**
    - O(n) parsing for most constructs
@@ -242,7 +246,7 @@ The architecture supports extensions via:
 3. **Effect Extensions**: New computational effects
 4. **Backend Extensions**: Additional compilation targets
 
-## Security Considerations
+## Security Considerations (planned)
 
 1. **Input Validation**
    - Unicode homograph detection
diff --git a/glyph-escapes.md b/glyph-escapes.md
index b9992c2..c3158e4 100644
--- a/glyph-escapes.md
+++ b/glyph-escapes.md
@@ -1,10 +1,16 @@
 # MPL Glyph Escape Sequences
 
-This document provides the authoritative mapping between ASCII escape sequences and UTF-8 glyphs for the Mathematical Programming Language (MPL).
+This document is the authoritative mapping between ASCII escape sequences and
+UTF-8 glyphs for the Mathematical Programming Language (MPL). It matches the
+lexer rules in [`src/main/antlr4/MPL.g4`](src/main/antlr4/MPL.g4) exactly:
+every escape below is accepted by the lexer, and no other escapes exist.
 
-## Core Mathematical Symbols
+Each glyph has **exactly one** ASCII escape (One Right Answer). Symbols that
+are plain ASCII (`; = < > + - ( ) [ ] { } : , _ | /` and the keywords
+`true`/`false`) need no escape and have none.
+
+## Greek Letters (Variables)
 
-### Greek Letters (Variables)
 | ASCII Escape | Unicode | Glyph | Usage |
 |-------------|---------|-------|-------|
 | `\alpha` | U+03B1 | α | Variable |
@@ -17,12 +23,12 @@ This document provides the authoritative mapping between ASCII escape sequences
 | `\theta` | U+03B8 | θ | Variable |
 | `\iota` | U+03B9 | ι | Variable |
 | `\kappa` | U+03BA | κ | Variable |
-| `\lambda` or `\lam` | U+03BB | λ | Lambda/Function |
+| `\lambda` | U+03BB | λ | Lambda / variable |
 | `\mu` | U+03BC | μ | Variable |
 | `\nu` | U+03BD | ν | Variable |
 | `\xi` | U+03BE | ξ | Variable |
 | `\omicron` | U+03BF | ο | Variable |
-| `\pi` | U+03C0 | π | Variable/Constant |
+| `\pi` | U+03C0 | π | Variable |
 | `\rho` | U+03C1 | ρ | Variable |
 | `\sigma` | U+03C3 | σ | Variable |
 | `\tau` | U+03C4 | τ | Variable |
@@ -32,110 +38,94 @@ This document provides the authoritative mapping between ASCII escape sequences
 | `\psi` | U+03C8 | ψ | Variable |
 | `\omega` | U+03C9 | ω | Variable |
 
-### Set Theory
+## Type Symbols
+
+| ASCII Escape | Unicode | Glyph | Usage |
+|-------------|---------|-------|-------|
+| `\nat` | U+2115 | ℕ | Natural numbers |
+| `\int` | U+2124 | ℤ | Integers |
+| `\rat` | U+211A | ℚ | Rational numbers |
+| `\real` | U+211D | ℝ | Real numbers |
+| `\complex` | U+2102 | ℂ | Complex numbers |
+| `\bool` | U+1D539 | 𝔹 | Booleans |
+| `\bot` | U+22A5 | ⊥ | Bottom |
+
+## Logic and Sets
+
 | ASCII Escape | Unicode | Glyph | Usage |
 |-------------|---------|-------|-------|
-| `\emptyset` | U+2205 | ∅ | Empty set |
-| `\union` or `\cup` | U+222A | ∪ | Set union |
-| `\intersect` or `\cap` | U+2229 | ∩ | Set intersection |
-| `\subset` | U+2282 | ⊂ | Proper subset |
-| `\supset` | U+2283 | ⊃ | Proper superset |
 | `\in` | U+2208 | ∈ | Element of |
-| `\notin` | U+2209 | ∉ | Not element of |
-| `\subseteq` | U+2286 | ⊆ | Subset or equal |
-| `\supseteq` | U+2287 | ⊇ | Superset or equal |
+| `\emptyset` | U+2205 | ∅ | Empty set |
+| `\and` | U+2227 | ∧ | Logical and |
+| `\or` | U+2228 | ∨ | Logical or |
+| `\implies` | U+27F9 | ⟹ | Implication / guard arrow |
+| `\forall` | U+2200 | ∀ | Universal quantifier (iteration) |
 
-### Logic
-| ASCII Escape | Unicode | Glyph | Usage |
-|-------------|---------|-------|-------|
-| `\and` or `\wedge` | U+2227 | ∧ | Logical and |
-| `\or` or `\vee` | U+2228 | ∨ | Logical or |
-| `\not` or `\neg` | U+00AC | ¬ | Logical not |
-| `\implies` or `\Rightarrow` | U+27F9 | ⟹ | Implication |
-| `\iff` or `\Leftrightarrow` | U+27FA | ⟺ | If and only if |
-| `\forall` | U+2200 | ∀ | Universal quantifier |
-| `\exists` | U+2203 | ∃ | Existential quantifier |
+## Operations
 
-### Operations
 | ASCII Escape | Unicode | Glyph | Usage |
 |-------------|---------|-------|-------|
 | `\times` | U+00D7 | × | Multiplication |
-| `\div` | U+00F7 | ÷ | Division |
+| `\div` | U+00F7 | ÷ | Division (`/` is an ASCII alias) |
 | `\ast` | U+2217 | ∗ | Generic operator |
 | `\circ` | U+2218 | ∘ | Function composition |
 
-### Relations
+## Relations
+
 | ASCII Escape | Unicode | Glyph | Usage |
 |-------------|---------|-------|-------|
-| `\neq` or `\ne` | U+2260 | ≠ | Not equal |
-| `\leq` or `\le` | U+2264 | ≤ | Less than or equal |
-| `\geq` or `\ge` | U+2265 | ≥ | Greater than or equal |
+| `\neq` | U+2260 | ≠ | Not equal |
+| `\leq` | U+2264 | ≤ | Less than or equal |
+| `\geq` | U+2265 | ≥ | Greater than or equal |
 | `\approx` | U+2248 | ≈ | Approximately equal |
 | `\sim` | U+223C | ∼ | Similar to |
 
-### Special Symbols
+## Definition and Assignment
+
 | ASCII Escape | Unicode | Glyph | Usage |
 |-------------|---------|-------|-------|
-| `\leftarrow` or `\gets` | U+2190 | ← | Assignment |
+| `\leftarrow` | U+2190 | ← | Assignment |
 | `\coloneq` | U+225C | ≜ | Definition |
-| `\rightarrow` or `\to` | U+2192 | → | Function type |
 
-## Effect Extensions
+## Effect Operators
 
 | ASCII Escape | Unicode | Glyph | Usage |
 |-------------|---------|-------|-------|
 | `\raise` | U+21AF | ↯ | Raise exception |
-| `\handle` | U+21B4 | ↴ | Handle exception |
+| `\handle` | U+21B4 | ↴ | Handle exception (postfix) |
 | `\parallel` | U+2016 | ‖ | Parallel composition |
 | `\lceil` | U+2308 | ⌈ | Atomic section start |
 | `\rceil` | U+2309 | ⌉ | Atomic section end |
-| `\oplus` | U+2295 | ⊕ | Allocate resource |
-| `\ominus` | U+2296 | ⊖ | Release resource |
-| `\module` | U+1D49C | 𝓜 | Module declaration |
-| `\Leftarrow` | U+21D0 | ⇐ | Import |
-| `\Rightarrow` | U+21D2 | ⇒ | Export |
-| `\send` | U+21C0 | ⇀ | Send (network) |
-| `\receive` | U+21BD | ↽ | Receive (network) |
+| `\oplus` | U+2295 | ⊕ | Allocate resource (postfix) |
+| `\ominus` | U+2296 | ⊖ | Release resource (postfix) |
+| `\send` | U+21C0 | ⇀ | Send to channel: `⇀_ch expr` |
+| `\receive` | U+21BD | ↽ | Receive from channel: `↽_ch expr` |
+| `\trace` | U+270E | ✎ | Output / trace |
+| `\break` | U+29C8 | ⧈ | Breakpoint |
+| `\delay` | U+23F2 | ⏲ | Delay |
+| `\periodic` | U+27F3 | ⟳ | Periodic task |
 
-## Additional Operators
+## Modules and Metaprogramming
 
 | ASCII Escape | Unicode | Glyph | Usage |
 |-------------|---------|-------|-------|
-| `\langle` | U+27E8 | ⟨ | Choice type/angle bracket left |
-| `\rangle` | U+27E9 | ⟩ | Choice type/angle bracket right |
+| `\module` | U+1D4DC | 𝓜 | Module declaration |
+| `\Rightarrow` | U+21D2 | ⇒ | Export (module body follows) |
+| `\middot` | U+2027 | ‧ | Qualified module access |
 | `\path` | U+1F5AB | 🖫 | File path prefix |
-| `\up` | U+21E1 | ⇡ | Stream position up |
-| `\down` | U+21E3 | ⇣ | Stream position down |
-| `\swap` | U+21C6 | ⇆ | Atomic swap |
-| `\llangle` | U+27EA | ⟪ | Deep update path start |
-| `\rrangle` | U+27EB | ⟫ | Deep update path end |
 | `\ulcorner` | U+231C | ⌜ | Code quotation start |
 | `\urcorner` | U+231D | ⌝ | Code quotation end |
 | `\llcorner` | U+231E | ⌞ | Code evaluation start |
 | `\lrcorner` | U+231F | ⌟ | Code evaluation end |
-| `\query` | U+003F | ? | Introspection |
-| `\break` | U+2A08 | ⧈ | Breakpoint |
-| `\trace` | U+270E | ✎ | Trace/log |
-| `\delay` | U+23F2 | ⏲ | Delay |
-| `\periodic` | U+27F3 | ⟳ | Periodic task |
 | `\lbracket` | U+3014 | 〔 | RAII scope start |
 | `\rbracket` | U+3015 | 〕 | RAII scope end |
-
-## Type System Symbols
-
-| ASCII Escape | Unicode | Glyph | Usage |
-|-------------|---------|-------|-------|
-| `\nat` or `\N` | U+2115 | ℕ | Natural numbers |
-| `\int` or `\Z` | U+2124 | ℤ | Integers |
-| `\rat` or `\Q` | U+211A | ℚ | Rational numbers |
-| `\real` or `\R` | U+211D | ℝ | Real numbers |
-| `\complex` or `\C` | U+2102 | ℂ | Complex numbers |
-| `\bool` or `\B` | U+1D539 | 𝔹 | Booleans |
-| `\bot` | U+22A5 | ⊥ | Bottom type |
+| `\langle` | U+27E8 | ⟨ | Choice type start |
+| `\rangle` | U+27E9 | ⟩ | Choice type end |
 
 ## String Escape Sequences
 
-String literals in MPL support the following escape sequences within double-quoted strings:
+String literals in MPL support the following escape sequences within
+double-quoted strings:
 
 | Escape Sequence | Character | Description |
 |----------------|-----------|-------------|
@@ -153,18 +143,20 @@ Examples:
 - `"Unicode: \u{1F600}"` - Unicode emoji 😀
 - `"""Raw string - no \n escapes"""` - Raw multi-line string
 
+## Deferred to M1
+
+The following glyphs appeared in earlier drafts but are **not** part of the
+M0 grammar. Each returns only together with a defined semantic:
+
+∪ ∩ ⊂ ⊃ ⊆ ⊇ ∉ ¬ ⟺ ∃ ⇐ → ⇡ ⇣ ⇆ ⟪ ⟫ ∑ √ ² `?` `%`
+
 ## Usage Notes
 
 1. **Input methods:**
    - Direct Unicode input (recommended for supported editors)
-   - ASCII escape sequences (for compatibility)
-   - Editor-specific shortcuts (e.g., Ctrl+Alt+g → γ)
+   - ASCII escape sequences (for compatibility, work in any editor)
 
 2. **Lexer behavior:**
-   - Escapes are processed during tokenization
-   - Unknown escapes result in compilation error
-   - Mixed Unicode/ASCII in same file is allowed
-
-3. **Pretty-printing:**
-   - Always outputs Unicode glyphs (never escapes)
-   - Configurable fallback to ASCII for terminals without Unicode support
\ No newline at end of file
+   - Escapes are alternatives in the lexer rules, processed during tokenization
+   - Unknown escapes are a lexical error
+   - Mixed Unicode/ASCII in the same file is allowed
diff --git a/math_prog_lang.md b/math_prog_lang.md
index 74c13f3..d353733 100644
--- a/math_prog_lang.md
+++ b/math_prog_lang.md
@@ -1,180 +1,204 @@
 # Mathematical Programming Language (MPL)
 
-## Core Symbol Set
+This is the language specification. The single source of truth for what
+parses is the grammar, [`src/main/antlr4/MPL.g4`](src/main/antlr4/MPL.g4);
+every symbol and example below is part of the M0 grammar unless explicitly
+marked "M1".
+
+## Core Symbol Set (M0)
 
 ### Mathematical Foundation (LaTeX)
 - **Variables:** α,β,γ,δ,ε,ζ,η,θ,ι,κ,λ,μ,ν,ξ,ο,π,ρ,σ,τ,υ,φ,χ,ψ,ω
-- **Collections:** ∅,∪,∩,⊂,⊃,∈,∉,⊆,⊇
-- **Logic:** ∧,∨,¬,⟹,⟺,∀,∃
-- **Operations:** +,-,×,÷,∗,∘
+- **Collections:** ∅,∈
+- **Logic:** ∧,∨,⟹,∀
+- **Operations:** +,-,×,÷ (ASCII alias `/`),∗,∘
 - **Relations:** =,≠,<,>,≤,≥,≈,∼
-- **Functions:** f: A → B, λ
+- **Functions:** λ (calls are `f(a, b)`)
 - **Assignment:** ←
 - **Definition:** ≜
 - **Structure:** (),[],{},⟨⟩
 
-### Effect Extensions (11 new glyphs)
+### Effect Extensions
 - **↯** Raise exception
-- **↴** Handle exception  
+- **↴** Handle exception (postfix: `expr ↴ { ↯pattern ⟹ expr }`)
 - **‖** Parallel composition
-- **⌈⌉** Atomic section/lock
-- **⊕** Allocate resource
-- **⊖** Release resource
+- **⌈⌉** Atomic section/lock (optional subscript: `⌈…⌉_lock`)
+- **⊕** Allocate resource (postfix: `database ⊕`)
+- **⊖** Release resource (postfix: `conn ⊖`)
 - **𝓜** Module declaration
-- **⇐** Import
-- **⇒** Export  
-- **⇀** Send (network)
-- **↽** Receive (network)
+- **⇒** Export
+- **‧** Qualified module access (`Mathematics‧sin`)
+- **⇀** Send to channel (`⇀_ch expr`)
+- **↽** Receive from channel (`↽_ch expr`)
 
 ### Additional Operators
 - **⟨v|e⟩** Choice type (value or error)
-- **🖫** File path prefix
-- **⇡⇣** Stream positioning
-- **⇆** Atomic swap
-- **⟪⟫** Deep update path
+- **🖫** File path prefix (`🖫"file.txt"` or `🖫identifier`)
 - **⌜⌝** Code quotation
 - **⌞⌟** Code evaluation
-- **?** Introspection
 - **⧈** Breakpoint
-- **✎** Trace/log
+- **✎** Trace/log (the one output operator)
 - **⏲** Delay
 - **⟳** Periodic task
 - **〔〕** RAII scope
 
+### Reserved for M1 (not in the grammar)
+∪,∩,⊂,⊃,⊆,⊇,∉ (set algebra); ¬,⟺,∃ (extended logic); → (function
+types); ⇐ (import); ⇡⇣ (stream positioning); ⇆ (atomic swap); ⟪⟫ (deep
+update); ? (introspection); ∑,√,²,% (arithmetic extensions). Each returns
+only together with a defined semantic.
+
 ## Grammar
 
+The sketches below are illustrative; [`MPL.g4`](src/main/antlr4/MPL.g4) is
+normative.
+
 ### Basic Expressions
 ```
 expr ::= variable | literal | operation | function_call | block
 
-variable ::= α | β | γ | ... | ω
-literal ::= number | string | path | list | set
+variable ::= identifier | α | β | γ | ... | ω
+literal ::= number | string | path | list | set | record
 operation ::= expr OP expr
-function_call ::= f(expr, ...)
-block ::= { statement; ... }
+function_call ::= f(expr, ...)          -- the one call syntax; f() is legal
+block ::= { expr; expr; ... }           -- ; separates, trailing ; permitted
 ```
 
-### Statements
+### Expression Forms
 ```
-assignment ::= variable ← expr
-definition ::= variable ≜ expr  
-conditional ::= condition ⟹ expr
-iteration ::= ∀variable∈set: expr
+assignment ::= expr ← expr
+definition ::= expr ≜ expr
+conditional ::= (condition ⟹ result) | fallback     -- guarded alternatives
+iteration ::= ∀pattern∈domain: expr
+lambda ::= λpattern: expr | λpattern∈domain: expr
 parallel ::= expr ‖ expr
-atomic ::= ⌈expr⌉_lock
-exception ::= ↯expr | expr ↴ {↯e ⇒ handler}
+atomic ::= ⌈expr⌉ | ⌈expr⌉_lock
+exception ::= ↯expr | expr ↴ {↯pattern ⟹ handler; ...}
 ```
 
 ### Types
 ```
 basic_type ::= ℕ | ℤ | ℚ | ℝ | ℂ | 𝔹
-function_type ::= domain → codomain
 choice_type ::= ⟨type|type⟩
-effect_type ::= type^effect
+function_type ::= domain → codomain     -- M1
+effect_type ::= type^effect             -- M1
 ```
 
 ## Example Programs
 
+These are the ten programs in [`examples/`](examples/), verbatim; CI parses
+them on every push (`./gradlew parseExamples`).
+
 ### Hello World
-```
-✎"Hello, World!"
+```mpl
+-- Hello World example
+✎"Hello, World!";
 ```
 
 ### Factorial
-```
-factorial ≜ λn∈ℕ: n≤1 ⟹ 1 | n×factorial(n-1)
-result ← factorial(5)
-✎result
+```mpl
+-- Factorial example with proper precedence
+factorial ≜ λn∈ℕ: (n≤1 ⟹ 1) | (n×factorial(n-1));
+result ← factorial(5);
+✎result;
 ```
 
 ### File Processing with Error Handling
-```
-processFile ≜ λpath: 🖫path ↴ {
-    data ← readFile(path)
-    result ← transform(data)
-    writeFile(result, 🖫"output.txt")
+```mpl
+-- File processing with error handling
+processFile ≜ λpath: {
+    data ← readFile(🖫path);
+    result ← transform(data);
+    writeFile(result, 🖫"output.txt");
     ⟨"success"|"failed"⟩
-} ↴ {↯e ⇒ ⟨⊥|e⟩}
+} ↴ {↯e ⟹ ⟨⊥|e⟩};
 ```
 
 ### Concurrent Download
-```
+```mpl
+-- Concurrent download with parallelism
 downloadAll ≜ λurls: ∀url∈urls: (
     fetchData(url) ‖ processData(url)
-) ⟹ mergeResults()
+) ⟹ mergeResults();
 ```
 
 ### Module Definition
-```
+```mpl
+-- Module definition example
 𝓜 Mathematics ⇒ {
-    π ≜ 3.14159...
-    sin ≜ λx∈ℝ: ...
-    cos ≜ λx∈ℝ: ...
-}
+    π ≜ 3.14159;
+    sin ≜ λx∈ℝ: ⊥ {- implementation deferred until MPL executes -};
+    cos ≜ λx∈ℝ: ⊥ {- implementation deferred until MPL executes -}
+};
 
-angle ← π/4
-result ← Mathematics‧sin(angle)
+angle ← π/4;
+result ← Mathematics‧sin(angle);
 ```
 
 ### Resource Management
-```
+```mpl
+-- Resource management with RAII
 databaseQuery ≜ λquery: 〔
-    conn ← database ⊕
+    conn ← database ⊕;
     ⌈
-        result ← execute(conn, query)
-        ✎"Query executed"
+        result ← execute(conn, query);
+        ✎"Query executed";
         result
     ⌉_db_lock
-    conn ⊖
-〕
+    {- conn ⊖ happens automatically at end of 〔〕 -}
+〕;
 ```
 
 ### Metaprogramming
-```
+```mpl
+-- Metaprogramming with code quotation
 generateFunction ≜ λname: ⌜
     λx: x × 2
-⌝
+⌝;
 
-doubler ← ⌞generateFunction("doubler")⌟
-result ← doubler(21)
+doubler ← ⌞generateFunction("doubler")⌟;
+result ← doubler(21);
 ```
 
 ### Real-time System
-```
+```mpl
+-- Real-time scheduler with periodic tasks
 scheduler ≜ ⟳(
-    tasks ← getPendingTasks()
-    ∀task∈tasks: execute(task) ‖ monitor(task)
-    , 100ms
-)
+    tasks ← getPendingTasks();
+    ∀task∈tasks: execute(task) ‖ monitor(task),
+    100ms
+);
 ```
 
 ### Network Server
-```
+```mpl
+-- Network server with connection handling
 server ≜ λport: 〔
-    socket ← bind(port) ⊕
-    ∀request: (
-        data ← ↽_socket request
-        response ← processRequest(data)
+    socket ← bind(port) ⊕;
+    ∀request∈acceptLoop(socket): (
+        data ← ↽_socket request;
+        response ← processRequest(data);
         ⇀_socket response
     ) ‖ handleNext()
-    socket ⊖
-〕
+    {- socket ⊖ happens automatically at end of 〔〕 -}
+〕;
 ```
 
 ### Type-safe Database
-```
-User ≜ {name: String, age: ℕ∣age>0, email: String}
+```mpl
+-- Type-safe database with refinement types
+User ≜ {name: String, age: ℕ | age>0, email: String};
 query ≜ λtable∈Database: ∀row∈table: validateUser(row) ↴ {
     ↯"Invalid user" ⟹ ⊥
-}
+};
 ```
 
 ## Critical Implementation Decisions
 
 ### Lexical Layer
-- **Unicode Normalization:** NFC on ingest, reject mixed forms
-- **Symbol Input:** Cross-platform keymap (Ctrl+Alt+g → γ) + ASCII escapes (\gamma → γ)
-- **Semicolon handling:** Require explicit `;` everywhere except before `}`
+- **Unicode Normalization:** NFC on ingest, reject mixed forms (planned; the parser currently consumes code points as-is)
+- **Symbol Input:** ASCII escapes (\gamma → γ), exactly one per glyph; editor keymaps are future tooling
+- **Semicolon handling:** `;` has one role — it separates expressions in a sequence; a trailing `;` is permitted (so `;` before `}` is legal but not required)
 - **Comments:** `--` for single-line comments (to end of line), `{- ... -}` for multi-line comments (nestable)
 - **String Literals:** 
   - Standard strings: `"..."` with escape sequences (`\n`, `\t`, `\\`, `\"`, `\u{XXXXXX}`)
@@ -183,25 +207,31 @@ query ≜ λtable∈Database: ∀row∈table: validateUser(row) ↴ {
 - **Number Literals:** Decimal (`123`, `3.14`), hex (`0x1A`), binary (`0b1101`), with optional type suffixes later
 
 ### Operator Precedence Table
+
+Authoritative copy: [precedence.csv](precedence.csv).
+
 | Level | Operators | Associativity |
 |-------|-----------|---------------|
-| 9 | function application | left |
-| 8 | ↯ ✎ ? ⧈ ⏲ (prefix) | right |
-| 7 | ∘ | left |
-| 6 | × ÷ ∗ | left |
-| 5 | + - | left |
-| 4 | = ≠ < > ≤ ≥ ≈ ∼ | non-assoc |
-| 3 | ∧ | left |
-| 2 | ∨ | left |
-| 1 | ⟹ | right |
-| 0 | ← | right |
+| 11 | f(a, b) ‧ ⊕ ⊖ ↴{…} (postfix) | left |
+| 10 | ↯ ✎ ⧈ ⏲ - ⇀_ch ↽_ch (prefix) | right |
+| 9 | ∘ | left |
+| 8 | × ÷ ∗ | left |
+| 7 | + - | left |
+| 6 | = ≠ < > ≤ ≥ ≈ ∼ | non-assoc |
+| 5 | ∧ | left |
+| 4 | ∨ | left |
+| 3 | ⟹ | right |
+| 2 | \| (guarded alternatives) | left |
+| 1 | ← | right |
+| 0 | ≜ | right |
 | -1 | ‖ | left |
 | -2 | ; | left |
 
 ### Grammar Resolutions
-- **Block semantics:** Every statement returns value (ML-style)
-- **Conditional associativity:** Right-associative (a⟹b⟹c = a⟹(b⟹c))
-- **Choice type parsing:** Different tokens for |value vs |type contexts
+- **Block semantics:** Every expression in a sequence yields a value (ML-style)
+- **Conditional associativity:** ⟹ is right-associative (a⟹b⟹c = a⟹(b⟹c)); guarded alternatives chain left: (c₁ ⟹ r₁) | (c₂ ⟹ r₂) | fallback
+- **Choice type parsing:** one BAR token; the `|` inside ⟨a|b⟩ is the guarded-alternative level of the inner expression
+- **Brace disambiguation:** `{a: e, …}` record, `{a, b, …}` set (two or more elements), anything else (incl. `{}`, `{x}`) a block
 
 ### Type System Extensions
 - **Effect polymorphism:** `map : (A→ᴱ B) → List A →ᴱ List B`
@@ -262,13 +292,16 @@ map ≜ ΛA. ΛB. λf: A→ᴱ B. λxs: List A. …
 ```
 Γ ⊢ e₁ : α             Γ ⊢ e₂ : β           Γ ⊢ e₃ : β
 ─────────────────────────────────────────────────────────  (HANDLE)
-Γ ⊢ e₁ ↴ { ↯x ⇒ e₂ } : β  ▷  Eff = (Eff(e₁) - {Raise ε}) ∪ Eff(e₂)
+Γ ⊢ e₁ ↴ { ↯x ⟹ e₂ } : β  ▷  Eff = (Eff(e₁) - {Raise ε}) ∪ Eff(e₂)
 ```
 
-### M0 Exit Criteria
-1. All spec examples parse and pretty-print round-trip
-2. No shift/reduce conflicts in grammar
-3. 10,000 random token sequences don't crash parser
+### M0 Exit Criteria (all CI-enforced)
+1. Grammar compiles with zero ANTLR errors and zero warnings (`-Werror`)
+2. All ten example programs parse (`./gradlew parseExamples`)
+3. Every ```mpl code block in the documentation parses (`DocumentationTest`)
+4. Full test suite passes (`./gradlew test`)
+
+Deferred to later milestones: pretty-print round-tripping and parser fuzzing.
 
 ## Implementation Roadmap
 1. **M0:** ANTLR grammar + 500 LOC test suite
diff --git a/precedence.csv b/precedence.csv
index f564eff..824b974 100644
--- a/precedence.csv
+++ b/precedence.csv
@@ -1,13 +1,15 @@
 Level,Operators,Associativity,Description
-9,function application,left,Function call f(x) or f x
-8,"↯ ✎ ? ⧈ ⏲ (prefix)",right,Unary prefix operators
-7,∘,left,Function composition
-6,× ÷ ∗,left,Multiplication and division
-5,+ -,left,Addition and subtraction
-4,= ≠ < > ≤ ≥ ≈ ∼,non-associative,Comparison operators
-3,∧,left,Logical AND
-2,∨,left,Logical OR
-1,⟹,right,Implication
-0,←,right,Assignment
+11,"f(a, b)  ‧  ⊕  ⊖  ↴{…}",left,"Postfix operators: function call, qualified module access, resource alloc/release, exception handler"
+10,"↯ ✎ ⧈ ⏲ - ⇀_ch ↽_ch (prefix)",right,"Unary prefix operators (including unary minus) and channel operations"
+9,∘,left,Function composition
+8,× ÷ ∗,left,Multiplication and division (/ is an ASCII alias of ÷)
+7,+ -,left,Addition and subtraction
+6,= ≠ < > ≤ ≥ ≈ ∼,non-associative,Comparison operators
+5,∧,left,Logical AND
+4,∨,left,Logical OR
+3,⟹,right,Implication / guard arrow
+2,|,left,Guarded alternatives: (condition ⟹ result) | fallback
+1,←,right,Assignment
+0,≜,right,Definition
 -1,‖,left,Parallel composition
--2,;,left,Statement sequencing
\ No newline at end of file
+-2,;,left,Expression sequencing (trailing ; permitted)
diff --git a/road_map.md b/road_map.md
index 8f36481..510be0c 100644
--- a/road_map.md
+++ b/road_map.md
@@ -19,7 +19,7 @@ The ANTLR grammar (`MPL.g4`) successfully defines 70+ mathematical symbols and c
    - **Gap**: 100% of type system missing
 
 3. **Effect System Illusion**
-   - Examples: `↴ {↯e ⇒ handler}` implies exception handling
+   - Examples: `↴ {↯e ⟹ handler}` implies exception handling
    - Grammar: Just parses symbols as operators
    - Examples: `〔〕` claims automatic resource cleanup
    - **Gap**: 100% of effect semantics missing
@@ -177,8 +177,12 @@ public class SymbolicError {
 **Goal**: Rich set of mathematical functions without English names
 
 **Code Changes**:
-```mpl
--- Instead of "sort", "map", "filter":
+These signatures are a design sketch for a future milestone — the symbols
+(→, ↑, ∃?, 📖, ✍, ⊤) are not in the M0 grammar, so the block is fenced as
+plain text:
+
+```text
+-- Instead of "sort", "map", "filter":   (design sketch, not yet parseable)
 ↑: List α → List α  -- ascending order (up arrow)
 ∀→: (α → β) → List α → List β  -- universal transformation
 ∃?: (α → 𝔹) → List α → List α  -- exists predicate filter
diff --git a/src/main/antlr4/MPL.g4 b/src/main/antlr4/MPL.g4
index a55ab30..3753c46 100644
--- a/src/main/antlr4/MPL.g4
+++ b/src/main/antlr4/MPL.g4
@@ -366,7 +366,7 @@ COLON       : ':' ;
 COMMA       : ',' ;
 UNDERSCORE  : '_' ;
 BAR         : '|' ;
-MIDDOT      : '‧' ;
+MIDDOT      : '‧' | '\\middot' ;
 
 // Identifiers. A leading underscore is NOT allowed: subscripts such as
 // ⌉_db_lock and ↽_socket must lex as UNDERSCORE + IDENTIFIER, not as a
diff --git a/src/test/java/com/mpl/test/DocumentationTest.java b/src/test/java/com/mpl/test/DocumentationTest.java
index 0a6d3fb..ee75815 100644
--- a/src/test/java/com/mpl/test/DocumentationTest.java
+++ b/src/test/java/com/mpl/test/DocumentationTest.java
@@ -24,6 +24,17 @@ public class DocumentationTest extends MPLTestBase {
         assertAllMplBlocksParse(Paths.get("README.md"));
     }
 
+    @Test
+    public void testSpecCodeBlocksParse() throws IOException {
+        assertAllMplBlocksParse(Paths.get("math_prog_lang.md"));
+    }
+
+    @Test
+    public void testWhitepaperCodeBlocksParse() throws IOException {
+        assertAllMplBlocksParse(Paths.get("whitepaper", "mpl-whitepaper.md"));
+        assertAllMplBlocksParse(Paths.get("whitepaper", "mpl-whitepaper-appendices.md"));
+    }
+
     private void assertAllMplBlocksParse(Path doc) throws IOException {
         String content = Files.readString(doc);
         Matcher m = MPL_BLOCK.matcher(content);
diff --git a/src/test/java/com/mpl/test/LexerTest.java b/src/test/java/com/mpl/test/LexerTest.java
index c45fff3..62695ed 100644
--- a/src/test/java/com/mpl/test/LexerTest.java
+++ b/src/test/java/com/mpl/test/LexerTest.java
@@ -89,6 +89,7 @@ public class LexerTest extends MPLTestBase {
     public void testModuleAccess() throws IOException {
         assertTokenTypes("Mathematics‧sin",
             MPLLexer.IDENTIFIER, MPLLexer.MIDDOT, MPLLexer.IDENTIFIER);
+        assertTokenTypes("\\middot", MPLLexer.MIDDOT);
     }
     
     @Test
diff --git a/whitepaper/README.md b/whitepaper/README.md
index e1fc998..b574c2f 100644
--- a/whitepaper/README.md
+++ b/whitepaper/README.md
@@ -10,12 +10,12 @@ This directory contains the comprehensive academic whitepaper for the Mathematic
    - Complete academic whitepaper in Markdown format
    - Suitable for online viewing and conversion to other formats
    - Includes all sections from Abstract through Conclusion
-   - Features real-world application examples in 5 domains:
-     - Scientific Computing (ODE solvers)
-     - Financial Systems (Black-Scholes, VaR)
-     - Machine Learning (transformers, gradient descent)
-     - Distributed Systems (Raft consensus, KV stores)
-     - Quantum Computing (Grover's algorithm, teleportation)
+   - Features application sketches in 5 domains:
+     - Scientific Computing
+     - Data Processing
+     - Web Services
+     - Machine Learning
+     - Systems Programming
 
 2. **`mpl-whitepaper.tex`** 
    - Conference-ready LaTeX version (IEEE format)
@@ -25,12 +25,11 @@ This directory contains the comprehensive academic whitepaper for the Mathematic
 
 3. **`mpl-whitepaper-appendices.md`**
    - Comprehensive appendices with:
-     - Complete symbol reference (70+ symbols)
-     - Annotated example programs (10 examples)
+     - Symbol reference (pointing to the authoritative glyph-escapes.md)
+     - Annotated example programs
      - Grammar validation details
-     - Performance measurements
      - Implementation details
-     - Future extensions roadmap
+     - Pedagogy and envisioned pilot materials
 
 ## Whitepaper Structure
 
@@ -42,17 +41,17 @@ This directory contains the comprehensive academic whitepaper for the Mathematic
 6. **Implementation** - ANTLR grammar and parser details
 7. **Evaluation** - Completeness, performance, accessibility
 8. **Case Studies** - Concurrency, resources, metaprogramming
-9. **Real-World Applications** - Scientific, financial, ML, distributed, quantum
+9. **Real-World Applications** - Scientific, data, web, ML, systems
 10. **Limitations & Future Work** - Current gaps and research directions
 11. **Conclusion** - Vision for universal programming
 
 ## Key Features Documented
 
-- **70+ Mathematical Symbols**: Complete Unicode operators with ASCII escapes
-- **11 Effect Operators**: Novel symbols for exceptions, concurrency, resources
+- **70+ Mathematical Symbols**: Unicode operators, each with exactly one ASCII escape
+- **Effect Operators**: Novel symbols for exceptions, concurrency, resources
 - **24 Greek Variables**: Full Greek alphabet for identifiers
-- **Zero Ambiguities**: Validated grammar with precedence rules
-- **Paradigm Coverage**: Functional, imperative, concurrent, OO, metaprogramming
+- **CI-Validated Grammar**: Compiles with zero ANTLR errors and warnings; documented precedence
+- **Paradigm Coverage**: Functional, imperative, concurrent, metaprogramming
 
 ## Building the LaTeX Version
 
diff --git a/whitepaper/mpl-whitepaper-appendices.md b/whitepaper/mpl-whitepaper-appendices.md
index cd37cdd..895749c 100644
--- a/whitepaper/mpl-whitepaper-appendices.md
+++ b/whitepaper/mpl-whitepaper-appendices.md
@@ -2,127 +2,26 @@
 
 ## Appendix A: Complete Symbol Reference
 
-### A.1 Core Mathematical Operators
+The authoritative symbol table — every glyph, its single ASCII escape, and
+its Unicode code point — is maintained in one place:
+[`glyph-escapes.md`](../glyph-escapes.md). It matches the lexer rules in
+[`MPL.g4`](../src/main/antlr4/MPL.g4) exactly. A duplicate table here would
+drift; earlier versions of this appendix did exactly that.
 
-#### Greek Letters (Variables)
-All 24 Greek letters serve as single-character identifiers, following mathematical convention:
+In summary, the M0 symbol set comprises:
 
-| Symbol | ASCII Escape | Unicode | Mathematical Usage | MPL Usage |
-|--------|-------------|---------|-------------------|-----------|
-| α | `\alpha` | U+03B1 | Angle, coefficient | General variable |
-| β | `\beta` | U+03B2 | Angle, coefficient | General variable |
-| γ | `\gamma` | U+03B3 | Euler constant | General variable |
-| δ | `\delta` | U+03B4 | Small change | General variable |
-| ε | `\epsilon` | U+03B5 | Small positive | General variable |
-| ζ | `\zeta` | U+03B6 | Zeta function | General variable |
-| η | `\eta` | U+03B7 | Efficiency | General variable |
-| θ | `\theta` | U+03B8 | Angle | General variable |
-| ι | `\iota` | U+03B9 | Imaginary unit | General variable |
-| κ | `\kappa` | U+03BA | Curvature | General variable |
-| λ | `\lambda`, `\lam` | U+03BB | Eigenvalue | Lambda/function |
-| μ | `\mu` | U+03BC | Mean, measure | General variable |
-| ν | `\nu` | U+03BD | Frequency | General variable |
-| ξ | `\xi` | U+03BE | Random variable | General variable |
-| ο | `\omicron` | U+03BF | - | General variable |
-| π | `\pi` | U+03C0 | Pi constant | Variable/constant |
-| ρ | `\rho` | U+03C1 | Density | General variable |
-| σ | `\sigma` | U+03C3 | Standard deviation | General variable |
-| τ | `\tau` | U+03C4 | Time constant | General variable |
-| υ | `\upsilon` | U+03C5 | - | General variable |
-| φ | `\phi` | U+03C6 | Golden ratio | General variable |
-| χ | `\chi` | U+03C7 | Chi distribution | General variable |
-| ψ | `\psi` | U+03C8 | Wave function | General variable |
-| ω | `\omega` | U+03C9 | Angular velocity | General variable |
+- **24 Greek letters** (α…ω) as variables, with λ doubling as the lambda binder
+- **Logic**: ∧ ∨ ⟹ ∀
+- **Arithmetic**: + - × ÷ (ASCII alias `/`) ∗ ∘, with unary minus
+- **Comparisons**: = ≠ < > ≤ ≥ ≈ ∼
+- **Sets and types**: ∅ ∈ ℕ ℤ ℚ ℝ ℂ 𝔹 ⊥
+- **Definition and assignment**: ≜ and ←
+- **Output**: ✎ (the one output operator)
+- **Effects**: ↯ ↴ ‖ ⌈⌉ ⊕ ⊖ ⇀ ↽ ⏲ ⧈ ⟳ 〔〕
+- **Modules and metaprogramming**: 𝓜 ⇒ ‧ 🖫 ⌜⌝ ⌞⌟ ⟨⟩
 
-#### Logical Operators
-
-| Symbol | ASCII Escape | Unicode | Precedence | Associativity | Description |
-|--------|-------------|---------|------------|---------------|-------------|
-| ∧ | `\and`, `\wedge` | U+2227 | 3 | Left | Logical AND |
-| ∨ | `\or`, `\vee` | U+2228 | 2 | Left | Logical OR |
-| ¬ | `\not`, `\neg` | U+00AC | 8 | Prefix | Logical NOT |
-| ⟹ | `\implies`, `\Rightarrow` | U+27F9 | 1 | Right | Implication |
-| ⟺ | `\iff`, `\Leftrightarrow` | U+27FA | 1 | Right | If and only if |
-| ∀ | `\forall` | U+2200 | - | - | Universal quantifier |
-| ∃ | `\exists` | U+2203 | - | - | Existential quantifier |
-
-#### Arithmetic Operators
-
-| Symbol | ASCII Escape | Unicode | Precedence | Associativity | Description |
-|--------|-------------|---------|------------|---------------|-------------|
-| + | - | U+002B | 5 | Left | Addition |
-| - | - | U+002D | 5 | Left | Subtraction |
-| × | `\times` | U+00D7 | 6 | Left | Multiplication |
-| ÷ | `\div` | U+00F7 | 6 | Left | Division |
-| ^ | - | U+005E | 7 | Right | Exponentiation |
-| √ | `\sqrt` | U+221A | 8 | Prefix | Square root |
-| Σ | `\sum` | U+2211 | - | - | Summation |
-
-#### Set Theory Operators
-
-| Symbol | ASCII Escape | Unicode | Description |
-|--------|-------------|---------|-------------|
-| ∅ | `\emptyset` | U+2205 | Empty set |
-| ∈ | `\in` | U+2208 | Element of |
-| ∉ | `\notin` | U+2209 | Not element of |
-| ⊂ | `\subset` | U+2282 | Proper subset |
-| ⊆ | `\subseteq` | U+2286 | Subset or equal |
-| ∪ | `\union`, `\cup` | U+222A | Set union |
-| ∩ | `\intersect`, `\cap` | U+2229 | Set intersection |
-| \| | - | U+007C | Set size/cardinality |
-
-#### Comparison Operators
-
-| Symbol | ASCII Escape | Unicode | Precedence | Description |
-|--------|-------------|---------|------------|-------------|
-| = | - | U+003D | 4 | Equality |
-| ≠ | `\neq`, `\ne` | U+2260 | 4 | Not equal |
-| < | - | U+003C | 4 | Less than |
-| > | - | U+003E | 4 | Greater than |
-| ≤ | `\leq`, `\le` | U+2264 | 4 | Less or equal |
-| ≥ | `\geq`, `\ge` | U+2265 | 4 | Greater or equal |
-| ≈ | `\approx` | U+2248 | 4 | Approximately |
-
-### A.2 Programming Extensions
-
-#### I/O and Assignment
-| Symbol | ASCII Escape | Unicode | Usage | Example |
-|--------|-------------|---------|-------|---------|
-| ✎ | `\pencil` | U+270E | Output/print | `✎ "Hello"` |
-| ← | `\leftarrow`, `\gets` | U+2190 | Assignment | `x ← 42` |
-| → | `\rightarrow`, `\to` | U+2192 | Function type | `ℕ → ℕ` |
-| ≜ | `\coloneq` | U+225C | Definition | `fact ≜ λn: ...` |
-
-#### Exception Handling
-| Symbol | ASCII Escape | Unicode | Usage | Example |
-|--------|-------------|---------|-------|---------|
-| ↯ | `\lightning` | U+21AF | Raise exception | `↯"Error!"` |
-| ↴ | `\downarrow` | U+21B4 | Handle exception | `expr ↴ {handler}` |
-
-#### Concurrency
-| Symbol | ASCII Escape | Unicode | Usage | Example |
-|--------|-------------|---------|-------|---------|
-| ‖ | `\parallel` | U+2016 | Parallel composition | `task1 ‖ task2` |
-| ⇀ | `\send` | U+21C0 | Channel send | `value ⇀ channel` |
-| ↽ | `\receive` | U+21BD | Channel receive | `↽ channel` |
-
-#### Resource Management
-| Symbol | ASCII Escape | Unicode | Usage | Example |
-|--------|-------------|---------|-------|---------|
-| ⊕ | `\oplus` | U+2295 | Resource acquire | `file ← ⊕open(path)` |
-| ⊖ | `\ominus` | U+2296 | Resource release | `⊖file` |
-| 〔〕 | `\lbracket`, `\rbracket` | U+3014/5 | RAII scope | `〔resource ops〕` |
-
-#### Type Symbols
-
-| Symbol | ASCII Escape | Unicode | Type | Set Definition |
-|--------|-------------|---------|------|----------------|
-| ℕ | `\nat`, `\N` | U+2115 | Natural numbers | {0, 1, 2, ...} |
-| ℤ | `\int`, `\Z` | U+2124 | Integers | {..., -2, -1, 0, 1, 2, ...} |
-| ℚ | `\rat`, `\Q` | U+211A | Rational numbers | {p/q : p,q ∈ ℤ, q ≠ 0} |
-| ℝ | `\real`, `\R` | U+211D | Real numbers | Complete ordered field |
-| ℂ | `\complex`, `\C` | U+2102 | Complex numbers | {a + bi : a,b ∈ ℝ} |
-| 𝔹 | `\bool`, `\B` | U+1D539 | Booleans | {true, false} |
+Symbols reserved for M1 (∪ ∩ ⊂ ⊆ ∉ ¬ ⟺ ∃ → ⇐ ∑ √ ² % ? and friends) are
+listed at the end of `glyph-escapes.md`; they are not in the grammar.
 
 ## Appendix B: Annotated Example Programs
 
@@ -141,10 +40,10 @@ All 24 Greek letters serve as single-character identifiers, following mathematic
 #### Month 3: Variables and Arithmetic
 ```mpl
 -- Calculate rectangle area
-ℓ ← 5       -- length
-w ← 3       -- width  
-A ← ℓ × w   -- area formula
-✎ A         -- output: 15
+L ← 5;         -- length
+w ← 3;         -- width
+A ← L × w;     -- area formula
+✎ A            -- prints 15 (once MPL executes)
 ```
 **Annotations:**
 - `←` (left arrow): Assignment matches math notation
@@ -155,9 +54,10 @@ A ← ℓ × w   -- area formula
 #### Month 6: Loops and Summation
 ```mpl
 -- Sum numbers 1 to 10
-Σ ← 0
-∀ n ∈ [1..10]: Σ ← Σ + n
-✎ "Sum: " + Σ
+numbers ← [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
+total ← 0;
+∀ n ∈ numbers : total ← total + n;
+✎("Sum: " + total)
 ```
 **Annotations:**
 - `∀` (for all): Universal quantifier for iteration
@@ -168,10 +68,10 @@ A ← ℓ × w   -- area formula
 #### Month 6: Conditional Logic
 ```mpl
 -- Classify a number
-x ← -5
-x < 0 ⟹ ✎ "Negative"
-x = 0 ⟹ ✎ "Zero"  
-x > 0 ⟹ ✎ "Positive"
+x ← -5;
+(x < 0 ⟹ ✎"Negative") |
+(x = 0 ⟹ ✎"Zero") |
+(x > 0 ⟹ ✎"Positive")
 ```
 **Annotations:**
 - `⟹` (implies): If-then as logical implication
@@ -181,9 +81,9 @@ x > 0 ⟹ ✎ "Positive"
 #### Month 6: Recursion (Factorial)
 ```mpl
 -- Factorial function
-fact ≜ λn: n ≤ 1 ⟹ 1 ∣ n × fact(n - 1)
+fact ≜ λn: (n ≤ 1 ⟹ 1) | (n × fact(n - 1));
 
-✎ fact(5)  -- Output: 120
+✎ fact(5)  -- 120 (once MPL executes)
 ```
 **Annotations:**
 - `≜` (define as): Function definition
@@ -194,42 +94,38 @@ fact ≜ λn: n ≤ 1 ⟹ 1 ∣ n × fact(n - 1)
 ### B.2 Advanced Examples
 
 #### Quadratic Solver
-```mpl
--- Solve ax² + bx + c = 0
+The quadratic solver below is an M1+ design sketch — it uses ², √ and
+subscripts, which are not yet in the grammar, so it is fenced as plain text:
+
+```text
+-- Solve ax² + bx + c = 0   (M1+ design sketch, not yet parseable)
 quadratic ≜ λa,b,c:
-    Δ ← b² - 4×a×c
-    Δ < 0 ⟹ ✎ "No real solutions"
-    Δ = 0 ⟹ ✎ "One solution: " + (-b÷(2×a))
-    Δ > 0 ⟹ 
-        r₁ ← (-b + √Δ) ÷ (2×a)
-        r₂ ← (-b - √Δ) ÷ (2×a)
-        ✎ "Two solutions: " + r₁ + ", " + r₂
+    Δ ← b² - 4×a×c;
+    (Δ < 0 ⟹ ✎"No real solutions") |
+    (Δ = 0 ⟹ ✎("One solution: " + (-b÷(2×a)))) |
+    (Δ > 0 ⟹ ✎("Two solutions: " + ((-b + √Δ) ÷ (2×a)) + ", " + ((-b - √Δ) ÷ (2×a))))
 ```
 
 #### List Processing
-```mpl
--- Filter and map
-numbers ← [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
+Set comprehensions and `mod` are M1+ design sketches, so this block is
+fenced as plain text:
 
--- Get even numbers
-evens ← {n ∈ numbers | n mod 2 = 0}
-
--- Square them
-squares ← {n² | n ∈ evens}
-
-✎ squares  -- Output: [4, 16, 36, 64, 100]
+```text
+-- Filter and map   (M1+ design sketch, not yet parseable)
+numbers ← [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
+evens ← {n ∈ numbers | n mod 2 = 0};
+squares ← {n² | n ∈ evens};
+✎ squares
 ```
 
 #### Error Handling
 ```mpl
 -- Safe division with exceptions
-safeDivide ≜ λx,y: 
-    y = 0 ⟹ ↯"Division by zero!"
-    x ÷ y
+safeDivide ≜ λx, y: (y = 0 ⟹ ↯"Division by zero!") | (x ÷ y);
 
 -- Using with handler
 result ← safeDivide(10, 0) ↴ {
-    ↯"Division by zero!" ⟹ ✎ "Error caught"
+    ↯"Division by zero!" ⟹ ✎"Error caught";
     ↯e ⟹ ↯e  -- Re-raise other errors
 }
 ```
@@ -237,139 +133,132 @@ result ← safeDivide(10, 0) ↴ {
 #### Concurrent Downloads
 ```mpl
 -- Download multiple URLs in parallel
-urls ← ["http://a.com", "http://b.com", "http://c.com"]
+urls ← ["http://a.com", "http://b.com", "http://c.com"];
 
--- Launch parallel downloads
-∀ url ∈ urls: 
-    fetch(url) ⇀ results ‖
+-- Launch parallel downloads, sending each result to the results channel
+∀ url ∈ urls : ⇀_results fetch(url);
 
 -- Collect results
-∀ i ∈ [1..|urls|]:
-    data ← ↽results
-    ✎ "Downloaded: " + |data| + " bytes"
+∀ url ∈ urls : (
+    data ← ↽_results url;
+    ✎("Downloaded: " + size(data) + " bytes")
+)
 ```
 
 #### File Processing with RAII
 ```mpl
 -- Process file with automatic cleanup
 processFile ≜ λpath: 〔
-    file ← ⊕open(path)      -- Acquire
-    lines ← readLines(file)
-    
-    ∀ line ∈ lines:
-        words ← split(line, " ")
-        ✎ "Word count: " + |words|
-    
-    -- file automatically released here
-〕
+    file ← open(path) ⊕;    -- Acquire
+    lines ← readLines(file);
+
+    ∀ line ∈ lines : (
+        words ← split(line, " ");
+        ✎("Word count: " + count(words))
+    )
+
+    {- file automatically released here -}
+〕;
 ```
 
 ### B.3 Real-World Application Examples
 
 #### Data Analysis
-```mpl
--- Statistical analysis
+∑, √ and ² are M1, so the statistics sketch is fenced as plain text:
+
+```text
+-- Statistical analysis   (M1+ design sketch, not yet parseable)
 analyze ≜ λdata:
-    n ← |data|
-    μ ← (Σ x ∈ data: x) ÷ n        -- mean
-    σ² ← (Σ x ∈ data: (x-μ)²) ÷ n  -- variance
-    σ ← √σ²                         -- std dev
-    
-    ✎ "n=" + n + ", μ=" + μ + ", σ=" + σ
+    n ← |data|;
+    μ ← (∑ x ∈ data: x) ÷ n;
+    σ² ← (∑ x ∈ data: (x-μ)²) ÷ n;
+    σ ← √σ²;
+    ✎("n=" + n + ", μ=" + μ + ", σ=" + σ)
 ```
 
 #### Simple Web Server
-```mpl
--- HTTP server
-server ≜ λport: 
-    ∀ req ∈ listen(port):
-        -- Handle request in parallel
-        handleRequest(req) ‖
-        
+Record field access (`req.path`) is M1, so the HTTP-server sketch is
+fenced as plain text:
+
+```text
+-- HTTP server   (M1+ design sketch, not yet parseable)
+server ≜ λport: ∀ req ∈ listen(port): handleRequest(req) ‖ acceptNext();
+
 handleRequest ≜ λreq:
-    req.path = "/" ⟹ 
-        respond(200, "<h1>Welcome!</h1>")
-    req.path = "/api/data" ⟹
-        respond(200, getData())
-    true ⟹  -- default case
-        respond(404, "Not found")
+    (req.path = "/" ⟹ respond(200, "<h1>Welcome!</h1>")) |
+    (req.path = "/api/data" ⟹ respond(200, getData())) |
+    respond(404, "Not found")
 ```
 
 #### Machine Learning - Perceptron
-```mpl
--- Simple perceptron
-perceptron ≜ λweights,bias:
-    λinputs: 
-        z ← (Σ i ∈ [1..|inputs|]: 
-            weights[i] × inputs[i]) + bias
-        z > 0 ⟹ 1 ∣ 0  -- Step activation
+∑, indexing and field access are M1, so the perceptron sketch is fenced
+as plain text:
 
--- Training step
-train ≜ λp,inputs,target,α:
-    output ← p(inputs)
-    error ← target - output
-    
-    -- Update weights
-    ∀ i ∈ [1..|inputs|]:
-        p.weights[i] ← p.weights[i] + α×error×inputs[i]
-    
+```text
+-- Simple perceptron   (M1+ design sketch, not yet parseable)
+perceptron ≜ λweights, bias:
+    λinputs:
+        z ← (∑ i ∈ [1..|inputs|]: weights[i] × inputs[i]) + bias;
+        (z > 0 ⟹ 1) | 0   -- Step activation
+
+train ≜ λp, inputs, target, α:
+    output ← p(inputs);
+    error ← target - output;
+    ∀ i ∈ [1..|inputs|]: p.weights[i] ← p.weights[i] + α×error×inputs[i];
     p.bias ← p.bias + α×error
 ```
 
 ## Appendix C: Grammar Validation
 
-### C.1 ANTLR 4 Grammar Statistics
+### C.1 ANTLR 4 Grammar Validation
 
-**Grammar Metrics:**
-- Total Lines: 373
-- Parser Rules: 32
-- Lexer Rules: 89
-- Unique Operators: 71
-- Precedence Levels: 12
-- Unicode Code Points: 76
+The authoritative grammar is [`MPL.g4`](../src/main/antlr4/MPL.g4). Instead
+of quoting statistics that drift, CI enforces these properties on every push:
 
-**Validation Results:**
-```
-ANTLR 4.9.3 Grammar Analysis
-============================
-Grammar: MPL.g4
-Conflicts: 0
-Ambiguities: 0
-Left Recursion: Resolved
-Start Symbol: program
-Target: Java
-```
+- The grammar compiles under ANTLR 4.13 with **warnings treated as errors**
+  (`-Werror`), so left recursion, token shadowing and unreachable
+  alternatives fail the build
+- All ten example programs parse (`./gradlew parseExamples`)
+- Every ```mpl code block in the documentation parses (`DocumentationTest`)
+- Start symbol: `program`; target: Java
 
 ### C.2 Precedence Table
 
-Full precedence hierarchy with examples:
+Authoritative copy: [`precedence.csv`](../precedence.csv).
 
 | Level | Operators | Example | Parses As |
 |-------|-----------|---------|-----------|
-| -2 | `;` | `a; b; c` | `((a); b); c` |
+| 11 | `f(a,b)` `‧` `⊕` `⊖` `↴{…}` | `M‧f(x)⊕` | `((M‧f)(x))⊕` |
+| 10 | `↯ ✎ ⧈ ⏲ -` (prefix), `⇀_ch ↽_ch` | `✎ -a` | `✎(-a)` |
+| 9 | `∘` | `f ∘ g ∘ h` | `(f ∘ g) ∘ h` |
+| 8 | `×,÷,∗` | `a × b ÷ c` | `(a × b) ÷ c` |
+| 7 | `+,-` | `a + b - c` | `(a + b) - c` |
+| 6 | `=,≠,<,>,≤,≥,≈,∼` | `a < b = c` | Error (non-assoc) |
+| 5 | `∧` | `a ∧ b ∧ c` | `(a ∧ b) ∧ c` |
+| 4 | `∨` | `a ∨ b ∨ c` | `(a ∨ b) ∨ c` |
+| 3 | `⟹` | `a ⟹ b ⟹ c` | `a ⟹ (b ⟹ c)` |
+| 2 | `\|` | `a ⟹ b \| c` | `(a ⟹ b) \| c` |
+| 1 | `←` | `a ← b ← c` | `a ← (b ← c)` |
+| 0 | `≜` | `f ≜ g ≜ h` | `f ≜ (g ≜ h)` |
 | -1 | `‖` | `a ‖ b ‖ c` | `(a ‖ b) ‖ c` |
-| 0 | `←` | `a ← b ← c` | `a ← (b ← c)` |
-| 1 | `⟹` | `a ⟹ b ⟹ c` | `a ⟹ (b ⟹ c)` |
-| 2 | `∨` | `a ∨ b ∨ c` | `(a ∨ b) ∨ c` |
-| 3 | `∧` | `a ∧ b ∧ c` | `(a ∧ b) ∧ c` |
-| 4 | `=,<,>` | `a < b = c` | Error (non-assoc) |
-| 5 | `+,-` | `a + b - c` | `(a + b) - c` |
-| 6 | `×,÷` | `a × b ÷ c` | `(a × b) ÷ c` |
-| 7 | `^` | `a ^ b ^ c` | `a ^ (b ^ c)` |
-| 8 | `√,¬,↯` | `√√a` | `√(√a)` |
-| 9 | _(app)_ | `f g h` | `(f g) h` |
+| -2 | `;` | `a; b; c` | `(a; b); c` |
 
-### C.3 Ambiguity Resolution Examples
+### C.3 Disambiguation Rules
 
 **Lambda vs Variable λ**
-- Context: `λ` as operator vs Greek variable
-- Resolution: Grammar rule precedence
-- Test: `λ ← λx: x` parses correctly
+- Context: `λ` opens a lambda and is also a Greek variable
+- Resolution: one token (`LAMBDA_VAR`); the parser decides by position
+- Test: `λ ← λx: x;` parses (assign a lambda to the variable λ)
 
-**Application vs Multiplication**
-- Context: `f g` (application) vs `a × b`
-- Resolution: Whitespace-sensitive lexing
-- Test: `f g×h` parses as `App(f, Mul(g, h))`
+**Braces: record vs set vs block**
+- `{a: e, …}` is a record, `{a, b, …}` (two or more elements) is a set,
+  everything else — including `{}` and `{x}` — is a block
+- A singleton set literal cannot be written in M0 (documented in
+  DECISIONS.md)
+
+**The bar `|`**
+- One BAR token serves guarded alternatives; the `|` inside `⟨a|b⟩` is the
+  guarded-alternative level of the inner expression
 
 ## Appendix D: Symbol Pedagogy Guide
 
@@ -388,7 +277,7 @@ Full precedence hierarchy with examples:
 **Progressive Introduction**:
 1. Start with simple: `λx: x + 1`
 2. Multiple parameters: `λx,y: x + y`
-3. With conditions: `λn: n > 0 ⟹ n ∣ 0`
+3. With conditions: `λn: (n > 0 ⟹ n) | 0`
 
 #### Teaching ∀ (For All/Loops)
 **Physical Activity**: "Everyone Does"
@@ -400,9 +289,9 @@ Full precedence hierarchy with examples:
 - ∀ x ∈ {1,2,3}: means "do for 1, then 2, then 3"
 
 **Code Progression**:
-1. Simple iteration: `∀ n ∈ [1..5]: ✎ n`
+1. Simple iteration: `∀ n ∈ [1, 2, 3, 4, 5] : ✎ n`
 2. With accumulation: `∀ n ∈ list: sum ← sum + n`
-3. Nested loops: `∀ i ∈ [1..3]: ∀ j ∈ [1..3]: ✎(i,j)`
+3. Nested loops: `∀ i ∈ [1, 2, 3] : ∀ j ∈ [1, 2, 3] : ✎(i + j)`
 
 #### Teaching ✎ (Output)
 **Physical Activity**: "Pencil and Paper"
@@ -427,13 +316,13 @@ Full precedence hierarchy with examples:
 
 **Week 3: Control Flow**
 - ⟹ (if-then)
-- ∣ (else)
+- | (fallback: `(condition ⟹ result) | fallback`)
 - Simple conditions
 
 **Week 4: Loops**
 - ∀ (for all)
 - ∈ (element of)
-- Ranges: [1..10]
+- List literals: [1, 2, 3]
 
 **Week 5: Functions**
 - λ (lambda)
@@ -447,12 +336,13 @@ Full precedence hierarchy with examples:
 
 ## Appendix E: Implementation Details
 
-### E.1 Unicode Normalization
+### E.1 Unicode Normalization (planned)
 
-All input undergoes Unicode normalization to NFC:
+Input should undergo Unicode normalization to NFC before lexing. This is
+planned; the current parser consumes code points as-is:
 
 ```java
-// Ensure consistent handling
+// Planned: ensure consistent handling
 String normalize(String input) {
     return Normalizer.normalize(input, Normalizer.Form.NFC);
 }
@@ -464,22 +354,28 @@ Context-aware error reporting maintains symbol clarity:
 
 ```
 Error at line 3:14: Expected '⟹' after condition
-  x < 0 ∣ "negative"
+  x < 0 | "negative"
         ^
-Hint: Use '⟹' for if-then. '∣' is only for else-branches.
+Hint: A guard needs an arrow: (x < 0 ⟹ "negative") | fallback.
 ```
 
+(Illustrative; today the parser emits standard ANTLR diagnostics.)
+
 ### E.3 ASCII Escape Processing
 
-Flexible escape sequences with shortcuts:
+Each glyph has exactly one ASCII escape, defined as a lexer alternative
+(the full table is [`glyph-escapes.md`](../glyph-escapes.md)):
 
 ```antlr
-LAMBDA : 'λ' | '\\lambda' | '\\lam' ;
-FORALL : '∀' | '\\forall' | '\\all' ;
-IMPLIES : '⟹' | '\\implies' | '\\=>' ;
+LAMBDA_VAR : 'λ' | '\\lambda' ;
+FORALL     : '∀' | '\\forall' ;
+IMPLIES    : '⟹' | '\\implies' ;
 ```
 
-## Appendix F: Input Method Documentation
+## Appendix F: Input Method Documentation (envisioned)
+
+Only the ASCII escapes exist today; everything else in this appendix is
+tooling we want to build.
 
 ### F.1 Visual Palette
 
@@ -491,10 +387,11 @@ IMPLIES : '⟹' | '\\implies' | '\\=>' ;
 
 ### F.2 Text Shortcuts
 
-**Common Patterns**:
-- `\lam` → λ (shorter than `\lambda`)
-- `\all` → ∀ (shorter than `\forall`)
-- `->` → → (arrow shortcuts)
+The lexer accepts exactly one escape per glyph (`\lambda`, `\forall`, …).
+Editor-side auto-replace could additionally offer shorthand that expands to
+the glyph before the code ever reaches the lexer:
+
+- `\lam` → λ (editor expands; the lexer itself only accepts `\lambda`)
 - `:=` → ≜ (definition)
 - `!=` → ≠ (not equal)
 
diff --git a/whitepaper/mpl-whitepaper.md b/whitepaper/mpl-whitepaper.md
index 0639e12..0ef5476 100644
--- a/whitepaper/mpl-whitepaper.md
+++ b/whitepaper/mpl-whitepaper.md
@@ -6,7 +6,7 @@
 
 ## Abstract
 
-In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a complete, production-ready programming language can be built entirely from mathematical symbols while maintaining full expressiveness across all programming paradigms. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education.
+In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a programming language can be built entirely from mathematical symbols; the current milestone is a fully working parser, with execution to follow. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education.
 
 ## I. Introduction
 
@@ -98,7 +98,7 @@ MPL builds on established mathematical notation:
 - **Logical Operators**: ∧ (and), ∨ (or), ¬ (not), ⟹ (implies)
 - **Quantifiers**: ∀ (forall), ∃ (exists), λ (lambda)
 - **Relations**: =, ≠, <, ≤, ≈
-- **Arithmetic**: +, -, ×, ÷, ^, √
+- **Arithmetic**: +, -, ×, ÷ (^ and √ arrive with defined semantics in M1)
 - **Types**: ℕ (natural), ℤ (integer), ℝ (real), 𝔹 (boolean)
 
 ### B. Programming Extensions
@@ -111,7 +111,7 @@ MPL introduces intuitive symbols for computational concepts:
 - **Concurrency**: ‖ (parallel bars) for parallel execution
 - **Resources**: ⊕/⊖ (circled plus/minus) for acquire/release
 
-These symbols were chosen through extensive testing with educators and children, ensuring each passes the Fatima Test.
+These symbols were chosen to pass the Fatima Test; empirical validation with educators and children is planned, not yet performed.
 
 ### C. Real Code Examples
 
@@ -124,9 +124,9 @@ Here's "Hello World" in MPL – as simple as a hypothetical student's first prog
 A more complex example calculating rectangle area:
 
 ```mpl
-ℓ ← 5
-w ← 3
-A ← ℓ × w
+L ← 5;
+w ← 3;
+A ← L × w;
 ✎ A
 ```
 
@@ -136,27 +136,31 @@ A ← ℓ × w
 
 The MPL implementation consists of:
 
-- **ANTLR 4 Grammar**: 373 lines defining complete syntax
-- **Unicode Normalization**: Ensures é and é are treated identically
-- **ASCII Fallbacks**: Every symbol has text escapes (λ → `\lambda`)
-- **Multi-platform Support**: Runs on any Unicode-capable system
+- **ANTLR 4 Grammar**: the complete M0 syntax, compiled with warnings treated as errors
+- **ASCII Fallbacks**: every symbol has exactly one text escape (λ → `\lambda`)
+- **Multi-platform Support**: runs on any Unicode-capable system
+- **Unicode Normalization**: planned (the parser currently consumes code points as-is)
 
 ### B. Parser Validation
 
-- Zero ambiguities across all test programs
-- 12-level precedence hierarchy matching mathematical conventions
-- Round-trip testing between Unicode and ASCII forms
-- Tested on example programs
+Everything in this list is enforced by CI on every push:
 
-### C. Educational Tools
+- The grammar compiles with zero ANTLR errors and zero warnings
+- All ten example programs parse
+- Every ```mpl code block in the project documentation parses
+- The precedence chain is documented in `precedence.csv` and exercised by the test suite
 
-Beyond the core language, we've developed:
+### C. Educational Tools (envisioned)
+
+Beyond the core language, we envision:
 
 - Visual symbol palettes for beginners
 - Voice input for multiple languages
 - Handwriting recognition for natural input
 - Integration with standard editors
 
+None of these exist yet; today the ASCII escapes are the portable input method.
+
 ## VI. Evaluation
 
 ### A. Hypothetical Learning Journey
@@ -171,16 +175,16 @@ Hypothesis: First Program Time could be minutes rather than days.
 
 **Building on math knowledge**: They could apply familiar mathematical concepts:
 ```mpl
-ℓ ← 5
-w ← 3
-A ← ℓ × w
+L ← 5;
+w ← 3;
+A ← L × w;
 ✎ A
 ```
 
 **Advanced concepts**: Mathematical notation could make loops intuitive:
 ```mpl
-Σ ← 0
-∀ n ∈ [1..10]: Σ ← Σ + n
+total ← 0;
+∀ n ∈ [1, 2, 3, 4, 5] : total ← total + n
 ```
 
 **Potential outcome**: Students might progress from beginners to teaching others within a year.
@@ -201,10 +205,9 @@ We hypothesize that MPL could improve three key metrics:
 
 While human outcomes are primary, technical validation shows:
 
-- Complete coverage of programming paradigms
-- 70+ operators handling all computational needs
-- Successful parsing of complex real-world programs
-- No loss of expressiveness compared to English-based languages
+- The ten example programs cover functional, concurrent, resource-managed, metaprogramming and module-based code, and all parse in CI
+- Every symbol has exactly one meaning and one ASCII escape
+- The M0 grammar compiles with zero ANTLR errors and warnings
 
 ### D. Current Implementation Limitations
 
@@ -239,59 +242,59 @@ We hypothesize that pilot programs could reveal:
 
 ## VIII. Real-World Applications
 
-MPL's mathematical syntax proves powerful across domains:
+MPL's mathematical syntax proves powerful across domains. Every block below
+parses with the shipped M0 grammar (this is CI-checked); where richer
+notation (∑, √, ², subscripts, tuples) is planned for M1, the examples use
+plain M0 syntax instead.
 
 ### A. Scientific Computing
 
 ```mpl
--- Runge-Kutta ODE solver
-rk4 ≜ λf,y₀,t₀,t₁,h:
-    steps ← ⌊(t₁ - t₀) ÷ h⌋
-    evolve ← λ(t,y):
-        k₁ ← h × f(t, y)
-        k₂ ← h × f(t + h÷2, y + k₁÷2)
-        k₃ ← h × f(t + h÷2, y + k₂÷2)
-        k₄ ← h × f(t + h, y + k₃)
-        (t + h, y + (k₁ + 2×k₂ + 2×k₃ + k₄)÷6)
-    iterate(evolve, (t₀,y₀), steps)
+-- Fixed-step numerical integration (Euler method)
+euler ≜ λf, y, t, h, steps: ∀step∈countTo(steps): (
+    y ← y + h × f(t, y);
+    t ← t + h
+);
 ```
 
 ### B. Data Processing
 
 ```mpl
 -- Statistical analysis
-data ← loadCSV("measurements.csv")
-μ ← (Σ x ∈ data: x) ÷ |data|
-σ ← √((Σ x ∈ data: (x - μ)²) ÷ |data|)
-✎ "Mean: " + μ + ", StdDev: " + σ
+data ← loadCSV("measurements.csv");
+total ← 0;
+∀ x ∈ data : total ← total + x;
+μ ← total ÷ count(data);
+✎("Mean: " + μ)
 ```
 
 ### C. Web Services
 
 ```mpl
-server ← λport:
-    ∀request ∈ listen(port):
-        response ← handleRequest(request) ‖
-        send(response)
+server ← λport: ∀request ∈ listen(port): (
+    response ← handleRequest(request);
+    ⇀_client response
+) ‖ acceptNext();
 ```
 
 ### D. Machine Learning
 
 ```mpl
 -- Neural network layer
-layer ≜ λW,b,x: σ(W × x + b)
-    where σ ← λz: 1 ÷ (1 + e^(-z))
+σ ≜ λz: 1 ÷ (1 + exp(-z));
+layer ≜ λW, b, x: σ(W × x + b);
 ```
 
 ### E. Systems Programming
 
 ```mpl
 -- Resource management with RAII
-processFile ← λpath:
-    〔file ← ⊕open(path)
-     data ← read(file)
-     parse(data)〕
-    -- file automatically closed
+processFile ← λpath: 〔
+    file ← open(path) ⊕;
+    data ← read(file);
+    parse(data)
+    {- file automatically closed at end of 〔〕 -}
+〕;
 ```
 
 ## IX. Limitations and Future Work
@@ -300,10 +303,10 @@ processFile ← λpath:
 
 From parser to production:
 
-1. **M1 (2025)**: REPL with basic type inference
-2. **M2 (2026)**: Compiler, standard library, IDE integration
-3. **M3 (2027)**: Performance optimization, advanced types
-4. **M4 (2028)**: Production readiness, ecosystem tools
+1. **M1**: REPL with basic type inference
+2. **M2**: Compiler, standard library, IDE integration
+3. **M3**: Performance optimization, advanced types
+4. **M4**: Production readiness, ecosystem tools
 
 ### B. Research Directions
 
diff --git a/whitepaper/mpl-whitepaper.tex b/whitepaper/mpl-whitepaper.tex
index e53b007..bacf75b 100644
--- a/whitepaper/mpl-whitepaper.tex
+++ b/whitepaper/mpl-whitepaper.tex
@@ -81,7 +81,7 @@ developtheweb@protonmail.com}}
 \maketitle
 
 \begin{abstract}
-In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80\% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a complete, production-ready programming language can be built entirely from mathematical symbols while maintaining full expressiveness across all programming paradigms. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education.
+In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80\% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a programming language can be built entirely from mathematical symbols; the current milestone is a fully working parser, with execution to follow. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education.
 \end{abstract}
 
 \begin{IEEEkeywords}
@@ -223,7 +223,7 @@ MPL introduces intuitive symbols for computational concepts:
 
 \textbf{Resources}: ⊕/⊖ (circled plus/minus) for acquire/release
 
-These symbols were chosen through extensive testing with educators and children, ensuring each passes the Fatima Test.
+These symbols were chosen to pass the Fatima Test; empirical validation with educators and children is planned, not yet performed.
 
 \subsection{Real Code Examples}
 
@@ -236,9 +236,9 @@ Here's "Hello World" in MPL – as simple as a hypothetical student's first prog
 A more complex example calculating rectangle area:
 
 \begin{lstlisting}[language=MPL]
-ℓ ← 5
-w ← 3
-A ← ℓ × w
+L ← 5;
+w ← 3;
+A ← L × w;
 ✎ A
 \end{lstlisting}
 
@@ -246,11 +246,11 @@ A ← ℓ × w
 
 \subsection{Technical Architecture}
 
-The MPL implementation consists of an ANTLR 4 grammar spanning 373 lines defining complete syntax, Unicode normalization ensuring é and é are treated identically, ASCII fallbacks where every symbol has text escapes (λ → \texttt{\textbackslash lambda}), and multi-platform support running on any Unicode-capable system.
+The MPL implementation consists of an ANTLR 4 grammar defining the complete M0 syntax, ASCII fallbacks where every symbol has exactly one text escape (λ → \texttt{\textbackslash lambda}), and multi-platform support running on any Unicode-capable system. Unicode NFC normalization is planned.
 
 \subsection{Parser Validation}
 
-Validation shows zero ambiguities across all test programs, a 12-level precedence hierarchy matching mathematical conventions, round-trip testing between Unicode and ASCII forms, and testing on example programs.
+Continuous integration enforces that the grammar compiles with zero ANTLR errors and zero warnings, that all ten example programs parse, and that every MPL code block in the project documentation parses. The precedence chain is documented in \texttt{precedence.csv}.
 
 \section{Evaluation}
 
@@ -265,16 +265,16 @@ To illustrate MPL's potential impact, consider a hypothetical student's progress
 
 \textbf{Month 3}: She calculates areas using familiar math notation:
 \begin{lstlisting}[language=MPL]
-ℓ ← 5
-w ← 3
-A ← ℓ × w
+L ← 5;
+w ← 3;
+A ← L × w;
 ✎ A
 \end{lstlisting}
 
 \textbf{Month 6}: A student might master loops using mathematical notation:
 \begin{lstlisting}[language=MPL]
-Σ ← 0
-∀ n ∈ [1..10]: Σ ← Σ + n
+total ← 0;
+∀ n ∈ [1, 2, 3, 4, 5] : total ← total + n
 \end{lstlisting}
 
 \textbf{Month 12}: A student could teach younger students, forming a coding club. The potential transformation: from novice to mentor in one year.
@@ -295,26 +295,28 @@ MPL's mathematical syntax proves powerful across domains:
 
 \subsection{Scientific Computing}
 \begin{lstlisting}[language=MPL]
--- Numerical integration
-integrate ≜ λf,a,b,n:
-    h ← (b - a) ÷ n
-    Σ i ∈ [0..n]: 
-        xi ← a + i × h
-        f(xi) × h
+-- Fixed-step numerical integration (Euler method)
+euler ≜ λf, y, t, h, steps: ∀step∈countTo(steps): (
+    y ← y + h × f(t, y);
+    t ← t + h
+);
 \end{lstlisting}
 
 \subsection{Data Processing}
 \begin{lstlisting}[language=MPL]
 -- Statistical analysis
-μ ← (Σ x ∈ data: x) ÷ |data|
-σ ← √((Σ x ∈ data: (x-μ)²) ÷ |data|)
+total ← 0;
+∀ x ∈ data : total ← total + x;
+μ ← total ÷ count(data);
+✎("Mean: " + μ)
 \end{lstlisting}
 
 \subsection{Web Services}
 \begin{lstlisting}[language=MPL]
-server ← λport:
-    ∀req ∈ listen(port):
-        handleRequest(req) ‖
+server ← λport: ∀request ∈ listen(port): (
+    response ← handleRequest(request);
+    ⇀_client response
+) ‖ acceptNext();
 \end{lstlisting}
 
 \section{Limitations and Future Work}