feat(language-1.2): tokenizers over the native text laws (LM-01..LM-03, LM-13; part of #30)

[humuhumu33]

Part of #30: the tokenizer, its laws as LexLean source, and the four rows this slice implements (LM-01..LM-03, LM-13).

Built to the design comment on #30. The design still covers the whole family (context windows, text generators, text classifiers, adapters, composition, production); this PR ships only what it implements and registers only those rows, the way #89 and #91 land stage by stage. LM-04..LM-12 are not in model/ids.toml, SPEC.md §31, the feature suite, or the test inventory here: each later slice adds its rows with its implementation (R3), so no registered ID is unwired and the gates are meaningful on this branch.

What changes

The text laws are LexLean source (LM-13). language/text-1.2/library/ is an embedded language-1.2 project with one native lexlean/core-module/2 module, LexLeanText.lex.tex, exported once from a Lean file that is kept outside the tree (tests/text-laws/MIGRATION.md records the migration; the oracle directory is absent, and a case checks that no authored Lean file declares the LexLeanText namespace or lies under its module root). The module states encodeWith (longest_match), encodeBytes (byte_level), decodeWith, encodeText/decodeText through utf8Encode/utf8Decode, and proves roundtrip, in_range, text_roundtrip and their byte-level forms, parametric in the vocabulary, with axioms within propext, Quot.sound, Classical.choice. crates/lexlean/src/text_laws.rs reads the registry (language/text-1.2/library.toml) and the native data, requires every name the elaboration applies, and generates the library's Lean through the ordinary core backend; verify audits that Lean like every generated core module and compiles it into the olean root before any module that imports it. Nothing is spliced: a module that declares a tokenizer imports LexLeanText.LexLeanText.

A tokenizer elaborates in linking (LM-01). ir/semantic/language_model.rs: a tokenizer over a utf8_lines artifact of role vocabulary elaborates to pieces, size, encode, decode, encodeText, decodeText over the library's functions, checked again by the ordinary rules as derived declarations. A vocabulary of another role or schema, or a tokenizer with type parameters, is refused with LLT4006; a scheme outside byte_level/longest_match is a schema violation (LLT4001). No new diagnostic code (the design's LLT4013/LLT4014 collide with #78 and are not needed by this slice).

The laws are generated and kernel-checked (LM-02). The tokenizer generates roundtrip, in_range, and text_roundtrip as reasoning-style theorems, each proved by one library lemma after unfolding exactly the named derived definitions, under the tokenizer's exact axiom policy; the axiom audit covers them like every generated declaration (LLV7005 on an understated policy).

UTF-8 (LM-03). A vocabulary that does not decode under utf8_lines (invalid UTF-8, a CR, a missing final LF) fails by the artifact rules (LLR3008) before any byte is tokenized; encodeText is over string, and decodeText goes through utf8Decode, which refuses bytes that are not UTF-8 rather than transcoding them.

Document. The LaTeX document states the scheme, the vocabulary, the laws module, the elaboration, and the generated theorems; the vocabulary's pieces are never document text.

Production. The four text declarations have rows in language/production-1.2.toml, all formal-only (SPEC.md §17.13): a tokenizer's elaborated definitions apply the text-laws library, which no production target realizes, so a root whose closure reaches one fails; context windows, text generators and text classifiers are not elaborated by linking in this release. The oracle's non-overlap table lists the same four as not-runtime (version 3, OR-02). LexLeanText.lex.tex is committed in the authoring notation, written by lexlean fmt (AU-04).

Identity and records. semantic_ir 10 → 11, lean_backend 17 → 18, latex_backend 11 → 12; every language-1.2 lock, golden, calculus package, fixture, production export, and verification record is regenerated for the new compiler-semantics ID (47d53f0e… on the merged tree). The register holds 391 IDs (387 on main + 4).

Cases

crates/conformance/src/cases/language_models.rs: LM-01 (elaboration, generated Lean and document, refusals), LM-02 (Lean-backed: the models example with two tokenizers verifies, and an understated policy fails the audit), LM-03 (the three malformed vocabularies, the string-typed encodeText), LM-13 (the library is one native module, the registry lists only the laws module, the sources are embedded, every applied name is declared with an exact policy). The scenarios in features/suites/language-models.feature carry the same four rows.

History note

The first merge of main on this branch (9e260b2) resolved every conflict to the branch side and dropped #130, #135, #137, #143 and #147; 8363b43 restores the correct merge tree, the merge of #144 (b6c4ba2) is clean, and the merge of #152 and #156 (c876764) keeps both sides; the verifier's text-laws records then join the attestation through their own list, since #152 moved process_records to the end of the run. No history was rewritten.

🤖 Generated with Claude Code

[humuhumu33]

IR slice pushed — 40f60dc0 (11 files, +834/−28)

The second increment: the IR and checker layer the design describes, still without elaboration, backends, cases or the example.

What it adds

• Four closed declarations in lexlean/semantic-module/2 (crates/lexlean/src/ir/semantic.rs): Tokenizer (scheme byte_level | longest_match, vocabulary artifact), ContextWindow (capacity, overflow refuse | keep_last), TextGenerator (tokenizer, window, scorer, max_tokens, stop, policy greedy | sample { xorshift32, proportional }), TextClassifier (token counts into a [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics #29 model) — each with its closed member types beside the other family types, and each carrying the serde shape and doc-comment style its neighbours use.
• crates/lexlean/src/ir/semantic/language_model.rs (152 lines): the family module implementing the same function set model.rs and reasoning.rs do — node counts, type/binder/term traversal, and the construct names.
• The schema members in schemas/semantic-module-v2.schema.json, matching the Rust members.
• An arm at every traversal and disposition site across ir/semantic.rs, ir/semantic/{model,reasoning}.rs, backend/semantic{,/reasoning}.rs and production/{eligibility,lower,source,certificate}.rs.

One rule the first draft missed, and how it was caught. The initial cut used rest patterns (Tokenzier { .. }) in the production analysis. audit-production (PD-07, implemented in crates/model/src/exhaustive.rs, applied by xtask/src/audit.rs) refuses that: "a rest pattern would classify constructs by default", then "has no explicit production disposition". The house style differs by file — in production/*.rs the existing families use no rest pattern at all, while ir/ and backend/ do — so the fix spelled all 56 occurrences out in the three production files, matching their neighbours, and left the other files as the local style has it.

Verified on this commit (WSL, pinned Lean 4.32.1, ext4 checkout):

Gate	Result
cargo fmt --all -- --check	rc=0
cargo check --workspace --all-features	rc=0
cargo xtask validate-model	documents current, 375 ids, 80 codes, meta-gate and audits clean (R1); audit-production: every construct of 5 enums has an explicit disposition (PD-07)
cargo xtask validate-spec-links	375 table rows bijective with the register (RP-07)
cargo xtask check-test-inventory	588 tests = 181 + 407, disjoint, none lost (RP-13)
cargo test -p repo-conformance --test bdd	5 passed, 0 failed

Still draft, still red on CI, for the same single reason: conformance_lm_01…lm_12 are unwired, so every job that runs the workspace test set fails on them. Next slices: elaboration into definitions and theorems (which needs the open question below answered), then backend rendering, then the cases and the examples/text-models pipeline with its artifacts and negative fixtures, then the regeneration sweep.

Still open for the maintainers: where the universal laws are proved (emitted LexLeanText runtime versus a LexLean-authored lexlean.text library), and the renumbering of the two proposed codes LLT4013/LLT4014, which #78 has already taken.

[afflom]

Recorded under L0.4 of the completion plan #106 (open pull requests reviewed against R3–R6 and merged or closed).

---

Generated by Claude Code

[afflom]

Status check on #30 / this PR (L0.4 and L2.2 of #106), from reading the branch against main (c257a657).

What the branch holds, which the description above does not say: the registration (LM-01..LM-12), the IR slice (the four declarations and their family module), and slice B, the text laws as an embedded native library (LexLeanText, text_laws.rs, tests/text-laws/MIGRATION.md), with LM-13 wired. Cases LM-01..LM-12 are still unwired, so the branch is red by design; elaboration, the Lean and LaTeX backends, the cases, examples/text-models, the production text_rows, the two codes, and the sweep are not started. Nothing has been pushed since 14 October.

It conflicts with main in seven files: the register count in README.md, SPEC §31, repository.rs and spec_links.rs, plus ids.toml, conformance.rs and lib.rs. The counts settle once #101 (SP-13) and #102 (RB-09) merge, so merging main in before then would be done twice.

@humuhumu33 are you continuing #30? If yes, nothing from me; the above is the state to rebase from. If not, I will merge main into this branch once #101 and #102 are in (merge commit, no history rewritten) and take the next slice here, elaboration of the tokenizer (LM-01..LM-03) first, then the rest in the order the design lists. I will not touch the branch before one of those.

---

Generated by Claude Code

[humuhumu33]

Yes, continuing #30. I merge main into this branch myself (merge commit, no history rewritten) and recompute the register total against main's count in the four places it lives.

The next slice is the tokenizer elaboration (LM-01..LM-03), along the route from the 14 October comment on #30: the text laws stay authored once as Lean in a scratch directory outside the release tree, exported losslessly into native lexlean/core-module/2 data and committed as .lex.tex in the embedded project with its migration record (slice B); the generated 1.2 modules import that generated module, nothing is spliced as text. Then the rest in the order the design lists.

[humuhumu33]

Progress on the tokenizer slice (LM-01..LM-03 over the native text laws), as of e1e78a8 on this branch.

Landed

• The text laws are one native lexlean/core-module/2 module, language/text-1.2/library/src/LexLeanText.lex.tex, exported once from a Lean file that is not in the tree (the migration is recorded in tests/text-laws/MIGRATION.md). It states encodeWith/encodeBytes (the two closed schemes), decodeWith, encodeText/decodeText through utf8Encode/utf8Decode, and proves roundtrip, in_range, text_roundtrip and their byte-level forms, parametric in the vocabulary (List String), with axioms within propext, Quot.sound, Classical.choice. Checked under the pinned v4.32.1; by decide evaluates the encoders on concrete inputs.
• text_laws.rs loads the registry and the native data, requires every name the elaboration applies, and generates the library's Lean through the ordinary core backend; verify compiles that Lean into the olean root before any module that imports it, after the same source audit as every generated core module.
• A tokenizer elaborates in linking (ir/semantic/language_model.rs) to pieces, size, encode, decode, encodeText, decodeText over the library's functions, and generates the three laws as reasoning-style theorems, each proved by one library lemma after unfolding exactly the named definitions. A vocabulary of another role or schema, or a tokenizer with type parameters, is refused with LLT4006; a scheme outside the enumeration is LLT4001. The LaTeX document states the scheme, the vocabulary, the laws module, the elaboration, and the generated theorems.
• Cases LM-01, LM-02 (Lean-backed: verifies the models example with two tokenizers, then plants an understated axiom policy, LLV7005), LM-03, and LM-13 are wired. semantic_ir, lean_backend, latex_backend move to 11/18/12.

Merge repair. The first merge of main (9e260b2) took the branch side for every conflict and dropped #130 (PX-13, production-result/2), #135, #137, #143, #147 and the VERIFICATION entries. 8363b43 restores the correct merge tree (origin/main 26e4dea with the branch); the register is 395 IDs. No force push.

In progress. The regeneration pass for the new compiler-semantics ID (locks, goldens, calculus packages, fixtures, production export, verification records) ran through golden and calculus in WSL and stopped when WSL itself failed (Wsl/Service/E_UNEXPECTED); it resumes once WSL is restarted. Until that lands, CI on this branch fails on stale locks (LLC0102). After it: LM-02 under Lean, clippy, and the SPEC §17.12 "Text components" prose, which is still to be written.

[afflom]

Approved at 85886c355, as a non-author, on the head that ran.

CI. All 26 checks green on this head (host legs, examples, rest with LM-01..LM-03 and LM-13, the 14 Atlas jobs and atlas (join), repro, honesty). The head contains main c3905e7c (#158, #146, #159, #153), which is still main's tip.

What I read, against #30's first slice and the rules.

• No free-form prompt is semantic code, and a tokenizer elaborates, it does not splice. ir/semantic/language_model.rs elaborates a tokenizer over a utf8_lines artifact of role vocabulary into six ordinary definitions and three generated theorems that apply the embedded laws library, and the ordinary rules check them again (R8). The module imports the library's generated Lean once; the LM-01 case counts the import and asserts the six definitions' types (encode/decode over bytes, encodeText/decodeText over string).
• The laws are LexLean source. LexLeanText.lex.tex is one native lexlean/core-module/2 module in the notation, exported once by an exporter that is removed from the tree in the next commit (tests/text-laws/MIGRATION.md), and LM-13 checks that the library is one native module, the registry lists only it, the sources are embedded, and every applied name is declared with an exact axiom policy (R9).
• Refusals and bounds. A vocabulary of another role or schema, or a tokenizer with type parameters, is LLT4006; a scheme outside byte_level/longest_match is a schema violation; a vocabulary that is not valid UTF-8 lines fails by the artifact rules (LLR3008) before any byte is tokenized (LM-03); the four text declarations are formal-only in the production registry and not-runtime in the oracle's non-overlap table, so no production claim is made for them yet.
• Identity and records. semantic_ir 11→, lean_backend and latex_backend move once; every language-1.2 record was regenerated by the repository's writers on a tree that contains main, 2,175 files; languages 1.0 and 1.1 are byte-identical.

Not a close of #30. This is slice 1 (the DoD's tokenization and round-trip items); context windows, generators, classifiers, adapters, composition and the nondeterminism contract follow, and #30 stays open. The PR says so ("Part of #30"), and it registers only the rows it implements.

Not blocking. R3's order is only partly in the history (the family rows first, the case wiring after the implementation); the gates check existence, not order.

Merging with a merge commit pinned to this head. Every other PR with language-1.2 records regenerates once after this.

---

Generated by Claude Code