Clarify documentation and complete BitVec reconstruction

[dollspace-gay]

What changed

• rewrote code comments, examples, READMEs, and verification documentation in plainer technical language
• removed repetitive emphasis and formulaic prose while preserving generated requirement tables and golden fixtures
• completed Thermite's literal BitVec N reconstruction surface for wrapping arithmetic, unsigned comparisons, bitwise operations, shifts, division, remainder, casts, and boolean connectives
• encoded SMT-LIB's all-ones bvudiv-by-zero behavior explicitly because Lean BitVec division uses a different default
• migrated supported QF_BV clause attribution to the literal kernel-checked reconstruction profile
• pinned lean-smt to upstream PR #227's proof-bearing commit, removing the compiled BitVec.eq_eq_beq sorry
• updated the generated Thermite/SmtExport.lean fixtures and trust documentation

Why

The repository had accumulated dense, repetitive comments and documentation that obscured the actual invariants. The QF_BV exporter also covered only an arithmetic/comparison subset, leaving bitwise, shift, division, and remainder clauses solver-trusted. The pinned lean-smt revision additionally emitted a compiled sorry warning from its BitVec reconstruction module.

Thermite now handles its complete QF_BV term surface through direct literal BitVec N normalization proofs. This avoids relying on lean-smt's broader, still-partial bit-blast reconstructor and keeps the generated proof terms within the project's Lean axiom allowlist.

Impact

• comments and user-facing documentation are shorter and easier to audit
• every QF_BV operator emitted by Thermite's bit-vector engine has a corresponding literal Lean rendering
• the default Thermite Lean build emits no declaration uses sorry warning
• Thermite's Lean source tree contains no sorry or admit declarations
• supported QF_BV translation obligations report only {propext, Classical.choice, Quot.sound}

Validation

• cargo test --workspace --no-fail-fast
• cargo test -p forge --bin forge --no-fail-fast — 468 passed
• cargo test -p forge --test g1_gate --test metrics_dashboard --features bv --test bv_lowering -- --nocapture — live Z3-backed suites passed, including 16/16 BitVec tests
• cargo test -p thermite-lower --test l2_conformance -- --nocapture — 7/7 live Kani tests passed
• cargo test -p forge --test l2_check --test degrade_conformance -- --nocapture
• lake build — 1120 jobs, no sorry warning
• bash scripts/lean-axiom-probe.sh — all 11 theorem probes passed
• python3 -m unittest discover -s tooling/tests -p 'test_*.py' — 46 passed
• cargo fmt --check
• git diff --check