feat(language-1.2): context windows and greedy and seeded text generators (LM-04..LM-06; part of #30)

[humuhumu33]

Slice 2 of #30 (intent: #30 (comment)). Context windows and greedy and seeded text generators are now elaborated by linking: LM-04..LM-06 and the new code LLT4016. Register: 404 → 407.

Draft until certificate A (#157) and certificate B (#163) have landed. This moves the language-1.2 identity. After they land I merge main once, regenerate, and mark this ready once (#15's draft rule).

What it does

• context_window (capacity ≥ 1, refuse or keep_last) elaborates to W.capacity, W.fit and W.push over the text-laws library. (admit is a reserved name segment, hence fit.) It generates:

  • bounded and push_bounded: every admitted or pushed context fits;
  • exact: a context that fits is admitted unchanged;
  • suffix under keep_last, or refuses under refuse.

• text_generator names a prior tokenizer, a prior window, a prior stateless list uint32 -> list int model whose evidence discharges every runtime check, a prior uint32 stop token, and max_tokens ≥ 1. It elaborates to:

  • G.score;
  • the closed inductives G.End (stop, exhausted) and G.Failure (unknown_token, context_overflow, invalid_utf8);
  • G.run, the library loop, structural in max_tokens;
  • G.generateTokens and G.generate.

  It generates bounded (at most max_tokens tokens) and context_bounded (the run equals the run whose scorer is never consulted on a context that does not fit).

• Policies: greedy takes the first maximum and no seed. sample uses the closed xorshift32 and proportional members, takes the seed as its last input and returns the next seed.

• Axiom policies: both declarations gain an axioms policy, as tokenizer has, and the audit holds them to it.

• Refusals: capacity or max_tokens 0 is LLT4016. A member of the wrong kind is LLT4006.

• Laws: every law is one LexLeanText lemma applied after unfolding, exactly as the tokenizer's laws are. The lemmas are new declarations of the native module, added by the round trip from [v0.4] Add language-model semantic components and compositional text-processing pipeline #30. The second record in tests/text-laws/MIGRATION.md shows the export re-derived from the compiler-generated Lean: 198 declarations and 19,448 nodes, equal except for the decoder's Lean import and one hygienic binder name.

• Text classifiers stay unelaborated; slice 3.

Identity

• semantic_ir 12 → 13 and latex_backend 12 → 13, and the text library is extended. Every language-1.2 lock, golden, fixture, production export and verification record is regenerated.
• The merge of main (8765fee) took feat(core): derived rows are made by Lean's reserved-name actions and checked (SM-33, stage 2 of #91, part 1) #155's rename of the library's private names to _private.LexLeanText.LexLeanText.#0. It applies to the 21 private names this slice adds as well, and the new derived rows pass feat(core): derived rows are made by Lean's reserved-name actions and checked (SM-33, stage 2 of #91, part 1) #155's remade-row check (LM-04 under Lean).

Verified locally (WSL, pinned Lean 4.32.1)

• Regeneration: all steps green, including verify-examples (uor-atlas aside, as in slice 1).
• Gates: fmt, validate-model, validate-spec-links (407 rows), clippy -D warnings, the workspace tests, the bdd meta-gate, check-test-inventory, check-golden and check-calculus.
• One flaky test: in the workspace run, verify::operational::tests::a_hints_file_from_the_environment failed once. It read a garbled LEXLEAN_VERIFY_WIDTH, an environment race with a parallel test. It passed 3/3 alone, and this PR does not touch that file.
• Conformance:
  • LM-01..LM-06 and LM-13;
  • RP-01..RP-14;
  • AU-04, SM-16, SM-33, PD-01, OR-02, CL-13, RT-04, MD-01 and RS-04.
• Lean-backed cases:
  • LM-04: the windows' laws are kernel-checked, and an understated window policy is refused (LLV7005).
  • LM-05: the kernel evaluates each end and each failure on fixtures, and a wrong claim about a run fails verification.
  • LM-06: seeds 1 and 48 reproduce Marsaglia's sequence and the expected draws.

Left for later slices

• Slice 3: classifiers, adapters, composition, and the no-prompt-as-code audit.
• Slice 4: production (text_rows, rust-std/rust-core), examples/text-models end to end, and closing [v0.4] Add language-model semantic components and compositional text-processing pipeline #30.

🤖 Generated with Claude Code

[afflom]

main carries the v0.4 train as of 193cd2148 (#167): certificates A and B as data, #68's lean_backend identities (1.1 10, 1.2 20), SM-32, MD-13, the package scaffold slice, register 413.

Suggested order for the identity-moving regenerations, so each sweep runs once: #171 (BS-02, mine) goes next — it moves no language data, adds one register row (414) and the TokenAudit bootstrap records and export, about half an hour on the merged identity — then this PR regenerates everything once on top of it, then #172. I will say here when #171 is on main; #173 and #174 (no identity, no records) land in between and need nothing from you.

---

Generated by Claude Code

[afflom]

main now carries wave 2 as well (d51d9f223, #171: BS-02, #173, #174; register 414). Nothing else that moves records is queued ahead of you: regenerate this PR on d51d9f223 whenever you are ready, then #172 on top of it. If you are not around, I will take the regeneration of #176 myself after the next check-in, per the owner's rule that the release does not wait on availability; say here if you would rather I did not.

---

Generated by Claude Code