Advance G0 syntax, layer, and proof boundaries

[TsekaLuk]

Summary

• proposes LCP-0001 and draft LDR-0004 to close missing K0 syntax for aggregate construction, dereference, public lifetime relations, type invariants, and total contract expressions
• adds independent Node and Python source parsers, raw UTF-8 rejection, package-boundary checks, and closed ASR/Core schema probes
• corrects K0/MEM traceability to 69/69 indexed, 19 evidence-bearing, and 50 explicit gaps
• selects replay-compatible Lean 4.24.0 through LDR-0005 and adds four checked allocation-cell theorem fragments
• pins Lean, Rust/Cargo, lean4checker, the format2024 exporter, Nanoda, and GitHub Action commits

Governance

LCP-0001 remains PROPOSED and LDR-0004 remains DRAFT. This PR is experimental specification evidence, not self-approval by the generating AI. It requires LCP-008 independent adversarial review and a named-owner decision before acceptance.

No rule is promoted to STABLE. No compiler implementation is authorized.

Evidence

• npm test
• Node/Python parser agreement: 77/77 text cases and 2/2 invalid UTF-8 byte cases
• Node/Python Core executor agreement: 14/14
• layer-boundary probes: 69/69
• K0/MEM index: 69/69; executable evidence: 19/69; explicit gaps: 50
• npm run proof:check
• Lean kernel build and pinned lean4checker replay
• pinned format2024 export and independent Nanoda replay: 44,846 declarations, zero errors
• proof placeholders (sorry, admit, axiom) rejected by the validator
• generated lock/report hashes stable across repeated runs
• GitHub Actions run 31362954228: validate and proof-fragment both passed on Linux

Fingerprints

• new spec lock: sha256:88f11e7094c6dab5dee131b9c8e7f038d093f093276e631cfddfdc8c041eddf0
• ASR/Core schemas, grammar, lexical rules, package manifest, theorem ledger, toolchain lock, and conformance corpora change
• observable K0 runtime results do not change in the existing 14-vector subset

Gate impact

G0 remains FAIL.

• G0-02: dual parsing exists; resolved ASR, lowering, and full control semantics remain
• G0-03: unchanged blocker
• G0-04: indexing is complete; 50 evidence gaps and all stable promotions remain
• G0-06: proof toolchain is locked and independently replayed; 4 fragments exist, 0/9 full theorems
• G0-08: lexical/package/schema boundaries are exercised; resolved-ASR reachability remains

Tracks #1, #3, #5, #6, and #7. Closes none.