[humuhumu33]

Closes #112 (L1.1 of #106). Draft; base release/v0.5 at 2959a4db2. Register stays at 443.

What changes

SPEC.md §3 and §4, edited in spec/src/Chapter03.lex.tex and Chapter04.lex.tex with cargo xtask spec (replace-block twice, insert-after three times) and regenerated. README "What it does" gains one paragraph; CHANGELOG one entry.

§3, the output list gains item 7:

7. for each production root of a language-1.2 project, a Rust package for each of its targets with the certificates that bind it to the root (§17.13–§17.19, §24.7).

§3, two new paragraphs after "The document is a program.":

Production compilation is the path from a verified project to executable code. Each production root (§17.13) is lowered to a program of the production realization calculus (§17.14) and rendered to Rust (§17.16); kernel-checked certificates relate the root's meaning to the lowered program and to each rendering (§17.17), and export publishes the packages with that evidence (§24.7).

Production compilation exists so that every production root is certified optimal over its declared universe: a universe, a machine, and an objective fixed before any optimizer runs (§17.15), and a certificate whose premises cover every system of that universe (§17.18). A root is claimed optimal by its certificate and by nothing else; a root exported without one is certified to preserve its meaning and carries no optimality claim. §4.2 states what the guarantee never claims.

§4.1, after the list:

Language 1.2 additionally MUST support production compilation as §3 states it: production eligibility (§17.13), the production realization calculus (§17.14), GNAF requests and certification (§17.15, §17.18), the Rust backend (§17.16), semantic preservation (§17.17), the differential validation oracle (§17.19), and production export (§24.7).

§4.2, three items appended to the list (C3, C4, C5 of #106):

• a claim of optimality over an unrestricted program universe, every calculus program and every Rust program included, rather than over the universe a GNAF request declares (§17.15);
• a claim that representation minimality is execution optimality without a proved bridge (§17.18);
• a claim that a certificate establishes wall time on hardware, which is only measured and recorded as an open ledger row (§27.3).

Each qualification cites the rule that already enforces it: §17.15 validation rule 12 (uncovered_scope), §17.18 route 4 (bridge_missing, status representation_minimal), and §27.3 (an open measurement is never acceptance evidence).

IDs (RP-11)

No new IDs. The README paragraph ties the statement to the rows that carry it: PD-01..PD-08, TC-01..TC-07, RB-01..RB-14, SP-01..SP-20, PX-01..PX-13 for the path; GN-03 (universe fixed before any optimizer), GC-03, GC-04 (certificates over every system), PX-06 (export binds the evidence); GN-05 (no claim beyond the grammar universe) and GC-07 (bridge) for the qualifications. RP-11's capability table is unchanged and still claims every registered ID.

Why no register row (R3)

The amendment adds no capability and changes no behaviour; it states in §3 and §4 what §17.13–§17.19 and §24.7 already specify, as #231–#233 did for their prose sections. A row is the right carrier for the guarantee's enforcement, and that is #121 (L4.3): export requiring a global_optimal certificate, with PX-06 changed and a new error.

One wording choice for the maintainer

§24.7 and PX-06 treat GNAF evidence as optional at export today. A sentence "every production root is certified optimal" would contradict that. So §3 states the guarantee as the purpose of production compilation and says what holds now: a root is claimed optimal only by its certificate, and a root exported without one carries no optimality claim. This stays true after #121, which then removes the case. If you would rather §3 state the guarantee as a present MUST, say so and I will change the two sentences.

Sibling work

#113 (§2.3, §30 release identity) is in flight on the same line in another session. This PR touches only §3, §4, README "What it does" and the CHANGELOG top. The §4 headings still say "LexLean 1.0"; I left them, since release identity is #113's. If #113 lands first, this rebases on it; no register number is taken here, so nothing renumbers.

Gates run (WSL, at this head)

• cargo xtask validate-model: documents current, 443 IDs, every audit clean (deferral, source authority).
• cargo xtask validate-spec-links: 443 rows bijective.
• cargo fmt --all -- --check.
• conformance_rp_01..rp_16 and conformance_ns_01..ns_07: all pass. ns_01 (Lean verify of spec/) first failed with Lean's "failed to create thread" under my ulimit -v memory cap and passed on rerun without the cap at LEXLEAN_VERIFY_WIDTH=2.
• The regenerated SPEC.md differs from the base only in §3 and §4; no derived table moved.

Not run: clippy (no Rust changed), the bdd meta-gate (no feature file changed), the full just vv.

🤖 Generated with Claude Code

[afflom]

Maintainer: read, and in the release/v0.5 queue. The head is green and mergeable; keep it so. The release/v0.4 landings (#255 in regeneration now, then #259, #262, #264, #265, #293, the bootstrap trio #258/#266/#282, #247, #256, and #261) hold the gate and the review agents first, by the owner's direction. The v0.5 lane is reviewed in this order as agents free up: #285, #290, #286, #287, #288, #289. Nothing is needed from you on this one before the review.

---

Generated by Claude Code

[afflom]

Maintainer review of 2be3b42db: accepted as written. On the wording choice: keep §3 stating the guarantee as the purpose of production compilation with the present fact beside it. "Every production root is certified optimal" as a MUST would contradict §24.7 and PX-06 today; that MUST arrives with #121 and removes the case. The three §4.2 non-claims cite the rule that enforces each and sit in non-goals, so they qualify the guarantee the issue asks for rather than widen it. Citations check out on the line; §31 untouched; no row is right (R3). The §4 forward-merge from release/v0.4 touches §5 two lines below the last insertion, no overlap.

#285 merged into release/v0.5 just now (0694c7ca6) and both touch the CHANGELOG top; if GitHub reports a conflict, merge the line in (merge commit) and I merge on green; otherwise I merge as soon as the mergeability check settles.

---

Generated by Claude Code

[humuhumu33]

Merged release/v0.5 (bde798bd6, containing #285 and #287) into this branch with a merge commit, f060aab78; no rebase. GitHub now reports the PR mergeable and CI is re-running on the new head.

Only CHANGELOG.md conflicted, at the top of Unreleased. Resolved by keeping both entries: this PR's #112 entry above #285's #242 entry, nothing dropped. The #112 entry's closing count changed from "Register 443" to "Register 444", the count on the line since #287 (AU-14); this PR still adds no row. README.md and SPEC.md auto-merged with no conflict, and spec/src changed on one side only (this PR: Chapter03, Chapter04; the line: Chapter17, IdsAU), so no regeneration was needed.

Checked: git diff origin/release/v0.5 on the merge is the PR's original five files (CHANGELOG, README, SPEC.md §3/§4, Chapter03, Chapter04), 76 insertions and 9 deletions, SPEC.md hunks only in §3 and §4.

Not run: validate-model (NS-05) locally, because no regeneration was done; the SPEC.md text was merged by git, so CI's NS-05 is the first byte-for-byte check against the projection.

[afflom]

Maintainer: merged into release/v0.5 at e600b5829 (merge commit) and #112 closed by hand. The base merge at f060aab78 was the line and nothing else; 30 checks green.

---

Generated by Claude Code