spec: amend §C4 carve-outs — prelude.ail.json as compile-time-embed exception

Iter form-a.1 recon surfaced a load-bearing constraint the original
spec didn't anticipate: ailang-core embeds prelude.ail.json at
compile time via include_str! + serde_json::from_str (workspace.rs:417,
main.rs:474), and ailang-core cannot import ailang-surface to switch
the embed to .ail (crate-cycle, documented at loader.rs:9-13).

§C4 splits into two carve-out categories:
- (a) seven subject-matter carve-outs (unchanged, the original list)
- (b) one compile-time-embed carve-out: prelude.ail.json

Acceptance criteria #1, #2 and §T4 carve-out inventory test updated
from 7 to 8.

Roadmap: new [milestone] "Prelude embed: Form-A as compile-time source"
queued to retire §C4(b) by either splitting the workspace loader
(prelude-init moves to ailang-surface) or generating prelude.ail.json
via build.rs. examples/prelude.ail (rendered iter form-a.0) is the
dual-form symptom that milestone exists to resolve. Strike the [todo]
"Author examples/prelude.ail" entry — satisfied by iter form-a.0.

Re-grounding-checked PASS over six load-bearing assumptions (embed
sites verified at workspace.rs:417 + main.rs:474; crate-cycle
constraint real; eight carve-outs all on disk; prelude.ail green
under both roundtrip tests).

docs/specs/2026-05-13-form-a-default-authoring.md

@@ -227,10 +227,15 @@ property is replaced by parse-determinism plus idempotency — the
 two together discharge the load-bearing concern (hashing is well-
 defined for any `.ail` source).
 
-### C4. The seven carve-outs (immutable list)
+### C4. The carve-outs (immutable list)
 
-These seven files stay `.ail.json` post-milestone and gain no `.ail`
-sibling:
+Two structural reasons keep `.ail.json` alive post-milestone:
+(a) **subject-matter** carve-outs (seven files; the canonical
+list as drafted) and (b) **compile-time-embed** carve-outs (one
+file as of 2026-05-13; subject to a separate milestone). Both
+gain no `.ail` sibling.
+
+**(a) Subject-matter carve-outs (immutable, seven files):**
 
 ```
 examples/test_ct1_bare_xmod_rejected.ail.json
@@ -262,9 +267,54 @@ Justification per file:
   (changing the diagnostic) or refuse to encode at all (changing
   the test subject).
 
-The orchestrator agrees these are the only legitimate carve-outs.
-Any future addition to this list requires brainstorm-level
-justification on the same semantic grounds.
+**(b) Compile-time-embed carve-outs (one file as of 2026-05-13):**
+
+```
+examples/prelude.ail.json
+```
+
+Justification:
+- `prelude.ail.json` is `include_str!`-embedded at
+  `crates/ailang-core/src/workspace.rs:417` and
+  `crates/ail/src/main.rs:474`, then parsed via
+  `serde_json::from_str` at compile-time-fixed sites in production
+  code. Switching the embed to `prelude.ail` would require parsing
+  via `ailang_surface::parse`, but `ailang-core` cannot import
+  `ailang-surface` (crate-cycle constraint documented at
+  `crates/ailang-surface/src/loader.rs:9-13`). The mechanism is a
+  structurally distinct from the runtime-loaded-program corpus the
+  rest of this milestone migrates: `.ail.json` carve-outs in
+  category (a) are kept because their *content* cannot be expressed
+  in Form A; `prelude.ail.json` is kept because its *embed mechanism*
+  requires the JSON-AST form.
+
+  This is a real spec gap relative to §A4's authoring-doctrine
+  ("authors write `.ail`; the build derives the JSON-AST in-process
+  via `ailang_surface::parse`"). The prelude is currently authored
+  as `.ail.json` and embedded as bytes; the doctrine says it should
+  be authored as `.ail` and parsed at compile time. Resolving the
+  inconsistency requires either (i) splitting the workspace loader
+  so prelude-init lives in `ailang-surface`, (ii) generating
+  `prelude.ail.json` at build time from `prelude.ail` via a
+  `build.rs`, or (iii) some other refactor — all of which exceed
+  the scope of this milestone.
+
+  The resolution lives in a separate roadmap milestone:
+  **"Prelude embed: Form-A as compile-time source"** (see
+  `docs/roadmap.md`). After that milestone closes, this carve-out
+  category becomes empty and the spec text drops it.
+
+  Note: `examples/prelude.ail` was rendered in iter form-a.0 and
+  remains the authoring projection (it stays in the tree; both
+  forms coexist for prelude specifically, mirroring the iter-0
+  pilot's dual-form witness arrangement, until the
+  prelude-embed-refactor milestone resolves the inconsistency).
+
+**Future additions to either list require brainstorm-level
+justification on the same structural grounds** — not "this test
+is annoying to migrate" or "the diff is large", but a named
+mechanism (canonical-form rejection / compile-time embed / etc.)
+that the surface cannot satisfy.
 
 ## Data flow
 
@@ -409,21 +459,29 @@ as a follow-up rename.
 ### T4. Carve-out coverage check
 
 A new test `crates/ailang-core/tests/carve_out_inventory.rs`
-asserts that exactly the seven named carve-out files exist under
-`examples/*.ail.json` after milestone close. The test fails if a
-new `.ail.json` is added or a carve-out goes missing. The list
-is hardcoded in the test body — this is intentional: the carve-out
-list is part of the language's negative-test surface and any change
-to it is a deliberate, brainstorm-level decision.
+asserts that exactly the eight named carve-out files exist under
+`examples/*.ail.json` after milestone close (seven from §C4 (a) +
+one from §C4 (b)). The test fails if a new `.ail.json` is added
+or a carve-out goes missing. The list is hardcoded in the test
+body — this is intentional: the carve-out list is part of the
+language's negative-test surface and any change to it is a
+deliberate, brainstorm-level decision. The test's pass-count
+drops to seven once the prelude-embed-refactor milestone retires
+`prelude.ail.json` from category (b); the test body is then
+re-published with the smaller list in that milestone's iter.
 
 ## Acceptance criteria
 
 The milestone closes when all of the following are true:
 
-1. `ls examples/*.ail.json | wc -l` returns `7`, and the seven
-   files match the carve-out list verbatim.
-2. Every program in `examples/` other than the seven carve-outs
+1. `ls examples/*.ail.json | wc -l` returns `8`, and the eight
+   files match the carve-out list verbatim (§C4 category (a) +
+   category (b)).
+2. Every program in `examples/` other than the eight carve-outs
    exists as a `.ail` file with no `.ail.json` sibling.
+   `examples/prelude.ail` exists in addition to
+   `examples/prelude.ail.json` per §C4 (b) (dual-form for prelude
+   only, pending the prelude-embed-refactor milestone).
 3. The roundtrip-CI restatement (T1) is green: parse is
    deterministic, idempotent under print, CLI-pipeline idempotent,
    and the carve-out inventory test (T4) passes.