docs(yhwh): show the lambda Y combinator explicitly as the foundation

Y was named in the model but never shown as the formal symbol it is.
The Y combinator is the canonical operational name of self-reference;
without it visible, the four-phase mnemonic loses the anchor that
distinguishes mago-dbe from generic 'self-referential' branding.

- README hero: Y = λf. (λx. f (x x)) (λx. f (x x)) and the fixed-point
  equation Y f = f (Y f), with one-paragraph commentary on how mago-dbe
  materialises this at the type-system level (typed primitive-recursive
  analogue of an otherwise ill-typed combinator in System F).
- docs/YHWH.md §Y: same combinator and equation in a fenced block;
  explicit citation to Curry & Feys 1958; explicit correspondence
  Y f = f (Y f) ↔ G* = C[G*](M); explanation of why the typed,
  terminating, byte-stable variant differs from the untyped Y.

Curry & Feys 1958 was already in the SELF-HOST-PROOF bibliography;
this commit just makes the symbol visible at the front of the docs.

Author: roxdavirox

README.md

@@ -2,6 +2,12 @@
 
 A self-referential build model: **Y · Hydrate · Weave · Hatch**.
 
+```
+Y = λf. (λx. f (x x)) (λx. f (x x))                  Y f  =  f (Y f)
+```
+
+The first letter is the **Y combinator** (Curry & Feys, *Combinatory Logic* I, 1958) — the canonical name of self-reference computed without an external base case. mago-dbe materialises this fixed-point equation at the type-system level: the compiler `C` is typed by `G`, and `G = C(M)` is the output of `C` — proved unique, byte-stable, and sandbox-replicable in [`docs/SELF-HOST-PROOF.md`](docs/SELF-HOST-PROOF.md) (Theorem 5.1).
+
 The repo implements a spec/workflow engine that takes authored markdown intent and produces validated, typed, byte-stable runtime artefacts. The model name `YHWH` is read as a four-phase sequence — `Y` (self-reference), `Hydrate` (intent into structure), `Weave` (structure into composition), `Hatch` (composition into runtime). The internal project id is `mago-dbe`. The architectural pattern is formally proven self-hosted and metacircular at `bootstrap-complete-source` (v0.5.0).
 
 > **Honest floor.** The system does **not** learn, does **not** autonomously evolve, and does **not** synthesise new primitives. What it does is described and mapped to code in [`docs/YHWH.md`](docs/YHWH.md). What it provably does is in [`docs/SELF-HOST-PROOF.md`](docs/SELF-HOST-PROOF.md) (PhD-grade paper, 5 lemmas + theorem + physical-realisation argument).

docs/YHWH.md

@@ -32,6 +32,16 @@ What the system *does* converge toward is **self-compilation through specs**: ev
 
 > The Y combinator. The fixed point. The system emerging from its own definitional core.
 
+```
+Y = λf. (λx. f (x x)) (λx. f (x x))
+
+Y f  =  f (Y f)              -- the fixed-point equation
+```
+
+The first letter of the model is **the Y combinator** — Curry's untyped fixed-point operator (Curry & Feys, *Combinatory Logic* I, 1958). Given any function `f`, `Y f` produces an `x` such that `x = f x`. It is the canonical formal name of *self-reference computed without an external base case*; the regress is closed by structural duplication (`x x`) at the lambda level.
+
+mago-dbe materialises this combinator at the *type-system level*, not the value level. The compiler `C` is typed by `G`; `G` is the output of `C`; the equation `G = C(M, G)` holds at every iteration with `G* := C(M)` as its unique fixed point. The full formal correspondence — `Y f = f (Y f)` ↔ `G* = C[G*](M)` — is proved as Theorem 5.1 in [`SELF-HOST-PROOF.md`](SELF-HOST-PROOF.md). One-step convergence (Lemma 4.5) and acyclic primitive recursion (Lemma 4.4) replace the untyped recursion-via-self-application that makes `Y` ill-typed in System F: ours is a *typed*, *terminating*, *byte-stable* analogue of `Y`, restricted to a primitive-recursive transducer.
+
 The `Y` phase is the meta-circular fixed point: the compiler whose runtime types are produced by the compiler itself, given canonical source `M`. This is not a future feature; it is provably implemented and empirically verified across two physical sandboxes by SHA-256 equality across four independent measurements.
 
 | Concern | Implementation |