[v0.4] Certificate generation is bounded as SPEC §17.17 and SP-02 say, or they say how it is bounded (follow-up to #167) #178

Follow-up to #167 (reviews of #157 and #163). SPEC.md:4958-4963 says that each term, arm, encoder, function and the boundary of certificate A, and the terms and derivations of B, "are counted as they are built", and that generation stops with LLS8002 "as soon as a part is beyond the limit". The SP-02 statement says generating each certificate under the limit "stops it at the limit". On f1e1157:

• Certificate A is built whole and then weighed once: crates/lexlean/src/production/certificate.rs:539-552, generator.within(source.len(), "certificate A") after module_data.
• B's early abort counts 12 bytes a node (data_b/align.rs:100) while a record read takes about 35, so it can hold about three times the limit before it stops. Its final refusal is exact (data_b.rs:654).

No oversized certificate is accepted. The gap is the work and memory bound the text promises.

Definition of done:

• Either the A data writer and B's aligner count parts against max_file_bytes as they build, with a per-node weight that is a floor of the recorded notation, or §17.17 and the SP-02 statement say exactly what bounds generation (the lowering's lower bound, then a whole-certificate check) and how far past the limit a generator can get.
• A planted defect recorded in VERIFICATION.md: a root whose certificate passes the early bound but exceeds the limit is refused with LLS8002, and the record states the peak size held.
• No weaker gate; just vv green.

Generated by Claude Code