Admit the G0 service family on exact-word terminals, with the evidence 4b(4) requires

[briansrls]

Supersedes #11622's keyword-token implementation. The service family is admitted through a grammar terminal matching one exact word, so the twelve marker words stay ordinary identifiers everywhere else and the lexer gains no rule — which is the whole cost argument, since #11622 turned every plain-name slot into a thirteen-way choice and was measured raising eval steps on 192 existing witnesses with none falling.

The branch this was carried from did not compile

Worth stating plainly, because I cited it as "prepared work" and was wrong. dag_grammar_literal_terminal was called twelve times and declared nowhere — not on its own base, not on main:

error: effect summary incomplete: call to 'dag_grammar_literal_terminal' in
  v2.extdeps.languages.dag.dag_grammar_service_decl_expr
  has no established callee identity

I had verified that it merged main cleanly and never executed it. A clean merge of source that never compiled is not prepared work — the specification-without-execution trap §5 names. The roadmap row's citation is retracted in place, on the row.

Two things closed it, neither a language change:

• grammar_expr_literal_terminal already exists in v2.std.grammar; it wanted a local wrapper in this file's existing idiom, beside its sibling dag_grammar_terminal_lexeme.
• Seven marker words — service, operation, input, output, readonly, idempotent, hermetic — are reserved in the seed's dag_keyword_set, so ^service is not writable in .dag source at all: a caret literal takes an identifier and a keyword is not one. Those seven intern from their String spelling via symbol_intern_lexeme, which no keyword rule intercepts. G0 carries no keyword entry for any of them — which is the design, and what keeps the name-usability control meaningful.

Evidence

All 17 pre-existing claims execute green, including the full real access.PosixEffectivePrincipal service body — the leftover service token at dag/extdeps/access/posix_effective_principal_read_op.dag that this family exists to clear — and both normalized-tree door claims, so a parsed service is still refused before resolve and the fn control is still admitted through the same route. Parsing is not lowering.

Two repairs to the evidence itself

service_keywords_remain_usable_as_names_holds is restored. It had been retired as a §4b(4) climb, arguing the RED was no longer authorable. §4b(4) dissolves lower-rung production machinery and never the evidence, and §4b decides authorability at the fixture boundary, not the corpus boundary — plain source using the marker words as names is exactly source handed to the compiler by a fixture. It executes green. The superseded annotation is deleted rather than left beside the claim it argued against.

refuses was literally !parses, and parse_src folds tokenize and parse rejections into one Rejected — so all nine refusal claims were green whenever anything failed, the absorbing arm §5 refuses. refuses_at_parse requires tokenize to accept and parse to reject. All nine stay green under the pin, so they were refusing at the right door; that is now established rather than assumed.

The pin carries its own discriminating control, a_lexical_failure_is_not_a_parse_door_refusal_holds — a source that dies in the lexer is not a parse-door refusal. That also establishes by execution that the fixture fails at tokenize, since otherwise the claim would be red. Delete the tokenize arm and it goes red while all nine service refusals stay green.

Not in scope

Per the row's own out_of_scope: the evaluation-step cost of the whole-service witness. That is its own roadmap node and wants a matched-base re-measurement after the keyword machinery is gone — which this change is.

🤖 Generated with Claude Code