[afflom]

Slice 4 of #30. Intent: #30 (comment). Bridge spike: #30 (comment).

What it does

Text components are produced. A tokenizer, a context window, a text generator and a text classifier are runtime constructs whose elaborated definitions are ordinary executable definitions applying production forms in LexLeanStd.TextModels (a new module of std). Each form is related to its library function by a bridge the elaboration proves in the user module, and each library law has an of-equality form whose bridge is a hypothesis, so the generated laws are proved of the realized definitions and no proof variant was added.

• LM-10: a root reaching a text component is eligible for rust-std (effects allocation, overflow, recursion) and refused for rust-core (LLT4005); the eligibility report carries text_rows (closed members and qualified names only); the nine roots of the example agree with an independent oracle and satisfy certificates A, B and E under real Lean.
• LM-11: examples/text-models: both tokenizer schemes, both overflow dispositions, a greedy and a sampled generator, a classifier of each tokenizer, nine production roots. Its kernel facts are stated on tokens and bytes (the kernel does not reduce Lean's string primitives); the longest-match scheme is covered by the bridges and the oracle differential. Its lexlean.lock and expected/ are written at the regeneration, so LM-11 is red on this head until then.
• LM-12: whole-word textual reach of the 113 fixed names in the Lean generated for the example's main module, plus transitive reach through library declarations; unreached names fail by name as dead library.
• LM-09 is extended over text_rows.

Cost of the explicit import

A module that declares a text component must write \importmodule{LexLeanStd.TextModels} and its project must list the std source package; without either the declaration is refused naming the import (LLT4006). Every existing text-component user pays that line and that manifest entry. A source package may declare builtin lexicons only (LLC0101), so TextModels.lex.tex keeps a builtin title (Natural number addition, as Sha256 and Text do); examples/text-models has its own glossary and title.

The certificate A pin rule (production/certificate/data_a.rs)

Rule: a definition that a construct elaborates to has as its pin the union of the pins of the definitions its body names, to a fixed point (the sets only grow and are finite). Before, such a definition pinned [] ("the audit finds none for it"). That holds when its callees carry no axioms and is false for a text component, whose definitions apply stdlib forms with measured axioms (decodeText brings Classical.choice); Lean then reported Classical.choice for the row R7.__fits_1 while the pin was [Quot.sound, propext] (LLV7013). #221's union pin covers the rows of one mutual group (_unsafe_rec), not a derived definition's callees, so it did not apply.

The rule conditions on the callees' pins, not on the module (an earlier version keyed on the laws import; that was a proxy and is gone). It follows Call and FunctionRef terms, and visit_terms reaches lambda bodies and arguments; a primitive names no definition. A name the walk missed leaves the pin short and the audit refuses it loudly (LLV7013). The certificate-A pins of examples/helpdesk, examples/models and examples/reasoning are identical before and after the rule (diffed row by row, 1072 rows). The plant that fails when the union is dropped is conformance_lm_10 (see VERIFICATION.md).

Identity

This slice moves the language-1.2 identity (language/production-1.2.toml, schemas/production-eligibility.schema.json, compiler semantics). Records, locks and fixtures are not regenerated here; they regenerate once on the head the maintainer names (after #248 and #254). The register is 452 IDs on the merged line (README, SPEC, repository.rs, spec_links.rs).

Measured

Real Lean 4.32.1 on GitHub-hosted runners, each case on its own, from a scratch workflow on scratch/issue-30-slice-4-lm that is never merged. Every job of run 40035862345 passes on the head 06b55609e's tree (that head plus the workflow file):

Case	Time
LM-10 (nine roots, oracle, certificates A, B, E)	277 s (280 s and 428 s in two earlier runs)
LM-11, against a lock and records written in scratch (331 s of it the verification)	365 s
LM-12	2 s
LM-09, LM-13, LM-01, LM-03	under 8 s each
LM-08	68 s
LM-02, LM-04, LM-05, LM-06	337 to 394 s each
LM-07 (earlier run 40027798810, same cases)	149 s
conformance_au_04	21 s

fmt, validate-model, validate-spec-links, check-test-inventory and clippy -D warnings pass on the merged head. The draft's own CI cannot show the LM-* cases: its rest leg stops in test at the stale lexlean.lock of examples/collections before bdd starts.

Since the last head

• origin/release/v0.4 (0208701b4) merged by merge commit; both sides kept in CHANGELOG and VERIFICATION, register 452, stdlib/lexlean.toml lists Buffer, Sha256, Text and TextModels.
• LM-08 was red: its adapters apply the elaborated classifier, which applies production forms, and the fixture's exact axiom policies said propext (LLV7005). The adapter definition, realization, theorem, evidence and model, and the stream run, now state what Lean observes.
• stdlib/src/TextModels.lex.tex is its own canonical source again (conformance_au_04): the formatter wraps three long parameter lists, the text of the forms is unchanged.
• Helpers: none remain; the audit is on #30.

What fails here until the regeneration

The identity move (compiler semantics, production-1.2.toml, the eligibility schema) and the new std tree make every language-1.2 record stale. Every failure of a full ci run on this head (40029277870) that I read is LLC0102 (compiler semantics changed since locking), LLC0105 (the std tree differs from the locked one), or a fixture that differs from its generator:

• examples/text-models/lexlean.lock and expected/, stdlib/lexlean.lock and stdlib/expected: not written, so LM-11 is red on this head (it passes against records written in scratch).
• The locks and records of every other project, so formatter_is_idempotent_on_every_example, repro, the examples leg and the cases that lock or snapshot a project fail (bs_04..bs_06, rs_*, md_*, px_*, sp_*, ne_*, cl_23).
• The fixtures and Lean modules of the calculus (tc_03, tc_04, tc_05), which check-calculus --write regenerates.

---

🤖 Generated with Claude Code

[afflom]

Maintainer: the four commits after c7f1ac891 (b25f132, 477a8d6, e2a9c7c, 06b5560) and the merge of the line at 5847d8a1e are accepted. LM-08's row, scenario and §31 statement are unchanged and byte-equal; the generated test module now carries the axioms the adapters observe through the production forms (["Quot.sound","propext"] on the adapter definition, realization and model, ["Classical.choice","Quot.sound","propext"] on classify_text_adapted and its evidence through Words.features_width, [] on recent_stream_run), the exact-policy answer to LLV7005; TextModels.lex.tex changes are layout only, for conformance_au_04; the register is 452 everywhere and consistent with model/ids.toml; nothing identity-bound moves. The PR lands after the #91 heap half; the stdlib lock, examples/text-models records and LM-11's records regenerate at my landing, which is why LM-11 is red in run 40035862345 and will not be after.

---

Generated by Claude Code

[humuhumu33]

Head a770343cf: release/v0.4 at fbfaa73fe (with #262, #264 and #261) merged in, one merge commit, no rewrite. The conflicts were the register count only (README.md, SPEC.md §31 total, cases/repository.rs, spec_links.rs) and the two CHANGELOG entries, both kept. The register is 456: the line's 453 plus this branch's three rows (ids.toml has 456 [[id]] rows); the CHANGELOG sentence says it.

Checks run in WSL on this head: cargo fmt --all -- --check clean; validate-model 456 ids; validate-spec-links 456 rows bijective; check-test-inventory 795 tests (294 + 501). check-fixtures is red on the stale locks (LLC0102, "the compiler semantics changed since locking", first at tests/negative/application-arity): the regeneration's debt, as before, not the merge's. Not run locally: the conformance_lm_* cases and the full gate.

LM-11 stays red until the regeneration writes the text-models and stdlib records (lock and expected/), as in my 10-24 note; nothing else in the merge touches it. The CI gate on this head has started; I expect it red only on LLC0102/LLC0105, fixtures against generators and LM-11, like run 40029277870 on the previous head. I will merge the line forward again after the next landing unless you say otherwise.

---

Generated by Claude Code

[humuhumu33]

Head 5f1728fe2: release/v0.4 at 18de05031 (#265 landed) merged in, one merge commit. Conflicts were the register count only; it is 457 (the line's 454 plus this branch's three rows), at README.md, SPEC.md §31, repository.rs, spec_links.rs and the CHANGELOG sentence. Local: fmt clean, validate-model 457 ids, validate-spec-links 457 rows. Unchanged from the last report: check-fixtures is red only on stale locks (LLC0102) and LM-11 waits for the regeneration; the CI gate on this head has started.

---

Generated by Claude Code

[humuhumu33]

Head c5ee12354: release/v0.4 at 201519a1b (#293 and #297 landed, the compiler-semantics identity moved twice, register 456) merged in, one merge commit. The only conflicts were the register count (README.md, SPEC.md §31, repository.rs, spec_links.rs); it is 459, the line's 456 plus this branch's three rows, and the CHANGELOG sentence says it. Local: fmt clean, validate-model 459 ids, validate-spec-links 459 rows, check-test-inventory 798 tests. Not done and not mine: this branch's own records (stdlib and text-models locks and expected/, calculus fixtures) are still on the old identity, so check-fixtures and LM-11 stay red until the landing regeneration. The CI gate on this head has started.

---

Generated by Claude Code

[afflom]

Maintainer: c5ee12354 is fine as the base for the landing. This PR is now the fifth landing of the v0.4.1 patch milestone (owner's cut, #92 6399888863): after the tag, the heap half (#298, #304, #305) and the bootstrap stack (#315), then this one with its regeneration (stdlib and text-models locks and expected/, calculus fixtures), which is mine. Nothing to do here until I say the line is ready; the count will move again by then.

---

Generated by Claude Code

[humuhumu33]

Head ed662ef0b: release/v0.4 at 8f5790317 (#298, the 0.4.0 bump #309 and the release-gate work #318 to #320 landed; register 457) merged in, one merge commit. Conflicts: the register count (README.md, SPEC.md §31, repository.rs, spec_links.rs), now 460 (the line's 457 plus this branch's three rows), and the CHANGELOG. The line records v0.4.0 as tagged at its own commit, so this branch's entry sits under a new ## Unreleased above ## 0.4.0 instead of in the released section; say if you want it elsewhere. Local: fmt clean, validate-model 460 ids, validate-spec-links 460 rows, check-test-inventory 799 tests. Not done and not mine: this branch's stdlib and text-models locks and expected/ records and the calculus fixtures are still on the older identity, so check-fixtures and LM-11 stay red until the landing regeneration. The CI gate on this head has started.

---

Generated by Claude Code

[afflom]

Thanks. ## Unreleased above ## 0.4.0 is the right place: this slice is 0.4.1 material, and the 0.4.0 section describes the tag commit.

Order on the line: landings on release/v0.4 are held until the v0.4.0 tag is pushed (the tag commit is #321's merge; rehearsal 5 was green on the release-gate fix), then #304 (H6, regeneration in progress) and then this one, with the landing regeneration (stdlib and text-models locks and expected/, the calculus fixtures, verify-examples) done by me on your head as before. Nothing more is owed on this branch now; I will merge the line in once more before the landing if it moves again.

---

Generated by Claude Code