The B4 door was one capability, not 40 diagnostics: the statement-form let has no body to lower from its own node

[briansrls]

The door was never 40 diagnostics. It was one missing capability.

Boundary 4 of the seven-boundary product receipt refused on the compiler's own 107-module closure with 40 diagnostics. b4 causal versus carried had already established, by reading the producers' return constructors, that 39 of those are produced on Accepted paths and merely carried into the Rejected list by rejected_with_pending — so exactly one rejects. What that reading could not do is name which one: body_lowering_reason_unsupported_form has sixteen producer sites and the receipt renders only a tally of reason symbols.

It is let lm = dag_language_model(). More precisely, it is the class that line belongs to: the ordinary statement-form let, which occurs at 104 sites in the tree.

What it refuses, read from the producers rather than from message text

v2.compiler.body_lowering_fold body_lower_let_expr calls body_lower_try_let_in_from_captured, whose first move is body_lower_let_in_body_capture_optional — a walk for the dag_token_kw_in atom. With no in it returns Accepted { value: Absent }, and body_lower_let_expr rendered that absence as unsupported_form.

Two independent confirmations that this is the statement form and not a failed spine walk, because the two have different repairs:

• The grammar says so by declaration. dag_grammar_let_expr is a choice of two alternatives: let n = e in e, which carries its own body, and let n [: T] = e, which does not.
• The parse tree says so by execution. fn f() -> Int { let x = 1 \n x } dumped through the real grammar gives a right-nested statement spine — stmt_seq.captured holds the let at grammar_sequence_left_node_projection and the continuation at grammar_sequence_right_node_projection.

So the statement form's Bind body is a sibling of the let, not a descendant of it. body_lower_let_expr was being handed a node that cannot in principle carry its own body. A refusal that fires on the ordinary case is a missing capability wearing a malformed-input costume.

What changed

1. The capability (body_lower_stmt_spine, body_lower_stmt_seq, reached from both body_lower_fold and the fn-body walker through one shared authority). A let-headed statement spine lowers to lower_bind(key, value, <remainder lowered>). It lives at dag_surface_stmt_seq because that is the only node from which both halves of a Bind are reachable — a structural argument, not a convenience one.

The guard is the whole overlap story: a spine is taken over only when it is headed by a statement-form let and has a following statement, which is exactly the case that has no lowering today. The in form is untouched and keeps its own path. A non-final statement that binds nothing refuses with its own cause (body_lowering_reason_statement_precedes_without_binding) rather than fabricating a continuation.

2. The cause split, which is worth landing on its own and would be even if the capability were bigger than it looked. body_lower_let_expr had one reason standing over "malformed let" and "well-formed let whose body this node cannot see". That conflation is what gave every reader the wrong first hypothesis and is why this took a session to find. It is #8801's split on the neighbouring form — spelled as two reasons rather than a coproduct-plus-projection because this result has exactly one consumer and it does not branch on the distinction; only the diagnostic does, and a coproduct whose sole consumer immediately collapses it would be a second representation of what the reason symbol already carries.

3. The instrument that made the finding reachable. The transaction now writes <txn>/b4-diagnostic-ledger.txt beside the retention census: every diagnostic the refusal carries, in carriage order, attributed through the same locus channel and production-identity vocabulary the census already used, plus a bounded rendering of the refused subtree's atoms. Written from inside the transaction for the same reason the census is. CensusOutcome is renamed B4EvidenceOutcome because boundary 4 now writes two evidence artifacts and one outcome type per artifact would be two names for one concept.

A note on why the atoms and not a file: a Node deliberately carries no filename — std.occurrence_identity occurrence_identity_scope_law names filename as a forbidden identity input — so nothing here proposes putting one on it. The atoms are a locator, not an identity.

The door moved — MOVED, and what it moved to

Both measurements are the same producer (run_seven_boundary_product_receipt), same subject (src/v2/compiler/00_compile.dag, 107 files), same transport.

	before	after
diagnostics	40	45
parse_grammar_choice_overlap_residue	7	7
body_lowering_reason_wrapper_retained_emitted	32	37
the one that rejects	body_lowering_reason_unsupported_form @ dag_surface_let_expr	normalized_tree_reason_wrapper_retention_not_normalized @ dag_surface_module

The 7 residue invariant holds, as its mechanism predicts. The next first failure is at a different producer, not one rank down a queue of lets.

And it changes the standing of the wrapper-retained population, which is the part a reader should not miss. The new holder is the normalized-tree admission refusing because retention is present. So the 37 are no longer merely carried beside the refusal — they are upstream of it. "Closing the 32 advances the door by zero boundaries" was true of the door as it stood and is not true of the door as it now stands; both prior probe documents are corrected in place rather than left to be reconciled by the next reader.

Evidence

src/v2/test/claim/body_lowering/statement_let_bind_test.dag, four claims written as invariants rather than as observations of the present frontier:

• statement_let_then_reference_lowers_holds — the positive control
• statement_let_chain_lowers_holds — nested binds
• single_statement_body_unchanged_holds — the path that already worked, unmoved
• unbound_statement_prefix_refuses_holds — the discriminating RED. A body whose non-final statement binds nothing has no continuation to bind and must refuse with its own cause. If this ever greens, the sequence lowering has begun inventing a body for a statement that produced none. It does not retire when the capability lands; it is the standing control that the capability stayed honest.

Executed before enrolment, through the real grammar and the real normalize: single-statement ACCEPTED; let x = 1 \n x ACCEPTED; let x = 1 \n let y = x \n y ACCEPTED; 1 \n 2 REJECTED: body_lowering_reason_statement_precedes_without_binding. The first pre-repair run of the same four returned unsupported_form on the two let cases.

Subject discipline, which cost another lane a run tonight

Every measurement here was taken through ctrl-build --remote, which fetches current main and applies the local worktree as a patch on top. The base commit is therefore not this branch's HEAD and differs between dispatches (three consecutive runs based on 08be45b6, 47ea349f, a9582f84). Pinning a sha would name a tree no run used, so the subject is stated as "current main at dispatch time, plus this branch's diff". A corollary worth carrying: a historical two-ref comparison is not available on this transport at all — positioning the worktree beforehand does not help, because the patch lands on whatever main is current.