feat(packages): the bootstrap pilot imports the stdlib; the vendored Text is deleted (PK-05, #161)

[afflom]

Closes #161

Second and last part of #161, on main ea0a4ed (which has #162: source packages, PK-01..PK-04, and the one language-1.2 identity move). This PR moves no identity; only bootstrap/'s records change.

What is here (PK-05, register 403)

• bootstrap/lexlean.toml declares stdlib as a source package (std); AxiomOutput imports LexLeanStd.Text and calls LexLeanStd.Text::…. bootstrap/src/Text.lex.tex (the vendored copy) is deleted.
• BS-01 loses vendored_text and its equivalence assertion, and asserts the project holds no Text of its own and links LexLeanStd.Text.
• Root lexlean-workspace.toml (members = ["bootstrap", "stdlib"]).
• P::bootstrap() stages bootstrap/, stdlib/ and the workspace file; xtask stages a project that declares source packages with the members it needs (check-golden, check-reproducibility, verify-examples).
• SPEC §17.23 and bootstrap/README.md no longer call anything temporary; SPEC §10.5 records that the two limits (version required in [[source_package]]; a package manifest declares builtin lexicon sources only and no artifact_source/[pdf]) are deliberate and what lifts them.
• bootstrap/ locks, oracles, verification records and the production-export packages are regenerated; nothing else moves.

Acceptance of #161, by item

• Fresh build and verify of an importing project succeeds offline: PK-03 (tests/packages/workspace) and BS-01 (bootstrap/ importing stdlib/), no network.
• A changed byte, a changed version, an undeclared package, a duplicate prefix and an escaping path each fail with a named code: PK-01 (LLC0105, LLC0105, LLC0106/LLR3009, LLC0107, LLS8001; also LLC0108 for the workspace rule). PK-02 covers LLR3009.
• The bootstrap/ pilot (feat(bootstrap): the axiom-output parser as language-1.2 source (BS-01) #160) and the stdlib (feat(stdlib): the first member, bytes and text over Bytes (#92) #153) use it; no vendored copy remains: PK-05.
• Languages 1.0/1.1 byte-identical; 1.2 identity regenerated once and recorded: check-golden leaves every 1.0/1.1 oracle untouched; the identity moved once, in feat(packages): source packages, a project imports the modules of a locked package (PK-01..PK-04) #162 (VERIFICATION.md, "source packages can fail").
• Full just vv: green on feat(packages): source packages, a project imports the modules of a locked package (PK-01..PK-04) #162's head; this PR's own run is the evidence for its head.

Local evidence

Linux x86-64, Lean 4.32.1: conformance_pk_01, pk_05, bs_01, sl_01, rp_07, rp_11, rp_14; validate-model (403 ids, 85 codes), validate-spec-links, check-test-inventory, check-golden, cargo fmt --check, clippy -D warnings.

---

Generated by Claude Code

[afflom]

Maintainer review: approved at 7440de2.

Checked against #161's acceptance, item by item, on this head (which contains main ea0a4eda; all 26 checks of the run are green, including the four host legs, examples and the Atlas shards):

• Fresh build/verify of an importing project, offline: PK-03 (feat(packages): source packages, a project imports the modules of a locked package (PK-01..PK-04) #162) and BS-01 here (check links LexLeanStd.Text, build, differential, plants) run with no network.
• Named codes for each refusal: PK-01/PK-02 (feat(packages): source packages, a project imports the modules of a locked package (PK-01..PK-04) #162) cover them; this PR adds nothing that weakens them, and bootstrap/lexlean.lock now carries the std pin.
• No vendored copy remains: bootstrap/src/Text.lex.tex is deleted, vendored_text() and its equality assertion are gone from BS-01, and PK-05 asserts the absence of the file, the declared package (std → stdlib), the workspace members, that LexLeanStd.Text is a module of the project with origin std, that the project's production roots are still exactly isClosedLeanName and parseAuditOutput (the stdlib's roots are not republished), and that neither the README nor SPEC §17.23 still describes a copy.
• Languages 1.0/1.1 byte-identical; 1.2 identity moved once: the identity moved in feat(packages): source packages, a project imports the modules of a locked package (PK-01..PK-04) #162; the diff here touches only bootstrap/ records, the package-export provenance of the bootstrap roots, and xtask staging.
• Full just vv: this run, green.

R3 order holds (register row + SPEC §31 row, scenario, conformance_pk_05, then the change); counts are 403 in all four places. The xtask change stages a project that declares source packages with the workspace file and the members it needs, so check-golden, check-reproducibility and verify-examples resolve packages exactly as in the checkout; projects without source packages take the old path unchanged. The two deliberate limits recorded in SPEC §10.5 (a required version; a package manifest declares builtin lexicon sources only) are stated with what lifts them and are not hidden defaults.

"Closes #161" is justified. Merging with a merge commit, pinned to this head.

---

Generated by Claude Code