Specify deterministic K0 name resolution and resolved ASR

[TsekaLuk]

Summary

• propose LCP-0002 and draft LDR-0006 for deterministic manifest-closed K0 name resolution
• define two-pass declaration collection, explicit namespace/visibility/scope rules, stable identities, and resolved function entry
• close the recursive resolved-ASR schema and audit symbol, local, lifetime, contract, brand, primitive, and entry closure
• add independent Node and Python resolver probes plus accept/reject/equivalence and semantic-tampering corpora
• update rule evidence, G0 reporting, lock data, roadmap, and blockers without changing the G0 FAIL or compiler No-Go decision

Evidence

• npm test passes
• 38/38 package-resolution inputs agree across independent implementations
• 11/11 accepted ASRs pass closed-schema validation and identity-closure audit
• 6/6 structurally valid ASR identity mutations reject
• 70/70 lexical/package/structural layer-boundary probes reject
• spec.lock and generated G0 report hashes are identical across consecutive runs
• K0/MEM traceability remains 69/69 indexed; evidence-bearing rules rise from 19 to 26 while 43 explicit gaps remain

Deliberate non-claims

• source byte spans and statically resolved field identities are still absent
• constant graph evaluation and cycle handling are still absent
• resolved-ASR-to-Core lowering and full static/dynamic semantics are still absent
• LCP-0002/LDR-0006 remain proposed/draft pending independent review
• G0 remains FAIL and durable compiler implementation remains unauthorized

Verification note

The local proof command could not start because Lake is not installed on this host. This PR does not change proof or proof-toolchain files; the parent PR proof-fragment check is green and this stacked PR CI must replay the locked Lean/Nanoda path.

Stack

Stacked on #8. Review and merge the parent first; do not merge this PR without independent semantic review.

[TsekaLuk]

Follow-up verification: workflow_dispatch run https://github.com/TsekaLuk/aether/actions/runs/31366473629 passed both jobs. The validate job regenerated spec.lock/G0 evidence with zero diff under Node 26.4.0 and Python 3.9.25; the proof-fragment job passed Lean build, pinned lean4checker replay, and pinned Nanoda replay. The preceding run exposed Python bytecode entering lock traversal; commit 3e6917d fixes the source/runtime-artifact boundary.