Enable strict record-field typecheck: close fail-open infer_record_lit hole (§5)

[gunbai-bot]

What

Closes the fail-open hole in the v1-seed typechecker's record-construction
path (infer_record_lit). Before this PR it silently accepted fields that
exist on no variant of the constructed type — a DESIGN.md §5 violation ("a
wrong answer is a loud error, never a warning"). That hole is exactly what
let the malformed BoolWitness { holds } rows (removed in #5272) typecheck
green.

Why it wasn't already strict — two resolver-precision gaps

The leniency was compensating for the resolver not being precise enough. Making
it strict required first making field-resolution confident, else real
constructions false-positive:

1. Aliases not followed — Set<T> = PointwisePower<T>; Set { member } is
   correct but the resolver returned Set's children, not PointwisePower's.
2. Variant-vs-collection name collisions — GrammarExpr.Optional (a
   variant) vs the Optional<T> collection; global lookup beat the
   expected-coproduct context.

Host change (src/v1/stage0/src/v1_compiler_infer.rs)

• record_lit_construction_field_names — a confident field-name resolver:
  follows type X = Y aliases and searches the expected coproduct's arms before
  the global fallback. Returns None when not confident, so anonymous /
  unresolved records never false-positive.
• field_in_any_variant_named — an ambiguity-aware secondary scan, run only
  on would-be-errors, suppressing the case where a field is valid on a
  same-named variant of another coproduct (e.g. TextNode) while keeping
  teeth on truly-undefined fields.
• Emits CompilerDiagnostic::FieldNotFound for an unknown constructed field.

Real bugs this surfaced (silently tolerated before)

The strict check immediately found pre-existing constructions with the wrong
field name — fixed here using the existing constructor helpers:

• infer_ground_add_mvp.dag: NodeLocus { node } → node_locus(node:) (field
  is anchor).
• 3 lens/application tests: PortLocus { port } → port_locus(port:) (field
  is anchor).

Proof by execution (§5: executed-clean, not sampled-clean)

Full claim_batch floor green against current main (merged in):
447 discriminating witnesses pass, zero field-not-found false positives.
Discriminating probe BoolWitness { holds } goes red with
field 'holds' not found in type 'BoolWitness'. The sampled sweep had called
the corpus clean; only the executed full floor surfaced the real bugs above.

Scope / stacking

• Depends on Delete malformed dead {holds} BoolWitness rows; re-home 5 dark signal predicates #5272 (dead {holds} removal). This branch carries those 2
  commits because the strict check reds on the {holds} rows until they're
  gone. If Delete malformed dead {holds} BoolWitness rows; re-home 5 dark signal predicates #5272 merges first I'll rebase to drop the duplicate; this PR
  otherwise subsumes it. Recommend merging Delete malformed dead {holds} BoolWitness rows; re-home 5 dark signal predicates #5272 first.
• Deferred: missing-required-field enforcement (the other half of the hole)
  — optional-cardinality + templating risk, unmeasured. Tracked separately.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed in 9737a87 + fb3a8d4 (rebased onto latest main; timeseries_signal_passives_test.dag conflict resolved by taking main's relocation + porting the holds-removal into the file main relocated those rows to, spice_passive_projection_test.dag).

§3/§7 port (the requested change). The strict infer_record_lit check now lives in the .dag authority src/v1/04_infer.dag; the committed src/v1/stage0/src/v1_compiler_infer.rs is the compiler's own emit of that source (derived, not hand-edited). Single-file seed diff (+136/-1, no new module deps) — only 04_infer.dag changed, so only its emitted module changes.

Tightened to confident-only (§5, no false positives). The first port false-positived on main's newer types where resolved field names diverge from source under newtype flattening / a §3 name collision:

• Watt = Measure<Power,One,Nat> etc. — concrete aliases of the single-field generic Measure<Q,S,M> { count: M }; the wrapper dissolves so count isn't in the resolved set.
• Vendor { legal_name } — extdeps Vendor<Domain> { legal_name } record vs the std Vendor = UnknownVendor | … enum; the name-keyed env grabs the enum.

record_lit_construction_field_names now fires only when the constructed name resolves to a plain, fully-grounded record (params == 0 && connective == Conj && children > 0), reading source field names from its own children. Generics, concrete aliases of single-field generics, and coproduct/enum (incl. the losing side of a §3 collision) all return none → silent. Full teeth retained on plain records, where every real bug lives.

§3 de-confliction. Two type TextFile collided in the bootstrap's combined src/v1+dsl closure (v1 {path, content} vs dsl/std {path, document}); renamed the dsl one → DocumentFile (it holds a Document, parallel to its sibling RenderedTextFile).

Proven by execution on the merged tree:

• floor (claim_executor over src/v2+dsl): 523 witnesses pass, 0 field-not-found false positives
• self-compile (src/v1+dsl via the regen path): 0 field-not-found
• cargo fmt --all --check + cargo clippy --all-targets -- -D warnings: clean
• discriminating probe: BoolWitness { holds: true } → error: field 'holds' not found in type 'BoolWitness'

— sent from silent-bee-439