[humuhumu33]

Part of #269: the reader of LexLean Rendering Expressions and the facts of a render (BS-26, lexicon/lre.rs: parse and the walkers of Render) as language-1.2 source, with roots parseLre and renderFacts of LexiconLre. It is the second slice of the lexicon.

Draft, stacked on #445 (BS-25). LexiconLre reads with LexiconLse's tokenizer and tree reader, as lre.rs reads with lse::read_tree, so it lands after #445.

Design

parseLre converts the tree the reader of BS-25 gives with a work stack that visits the operands of a form in the oracle's order and builds the form when they are on the value stack. renderFacts walks a render once, pre-order over an explicit stack whose steps the host bounds by the node count, and returns in one pass what the entry validator reads: the slots, renderer tokens, form and self-form references, and operator names in occurrence order, the first math-only construct, and the first script or fraction operand that renders nothing or is a bare script, with the oracle's message. Neither root admits recursion. The checks of those facts against the entry and the glossary stay in the host.

Evidence

Measured on the normative host on #445 over release/v0.4 at 4dc5b803c:

Leg	Runs	Agreed
named vectors, evaluator	88 (69 read, reaching all 27 listed refusals and the limit on nesting; 19 walked)	all
committed math renders, evaluator	216 reads, 216 walks	all
seeded renders and edits, evaluator	300 walks, 600 reads	all
vectors, renders and edits, pinned rustc	5,020	all
planted defects, each on its own named vector	20	all detected

Lean verifies the module, and the eligibility report gives each root exactly allocation and overflow. The first run found one plant whose vector did not reach it; VERIFICATION.md records it.

Gates at the head

cargo fmt --check, validate-model (480 IDs), validate-spec-links (480 rows), clippy on the workspace with -D warnings, and the 17 RP cases pass.

CI is expected red until the regeneration

The bootstrap/parse_lre and bootstrap/render_facts packages are not committed, so conformance_bs_26 stops at the stack-bound step after the differentials above have agreed. The regeneration owes them, the lock, the bootstrap expected/ records, and the recount of the bootstrap count cases. It is queued on the normative host after #445's.

🤖 Generated with Claude Code

[humuhumu33]

Landed in #480 (merge aaf845507 on release/v0.4), which carries this change with the BS-25..34 batch, regenerated together and verified by full gate run 43135541484. The branch is kept.