master red: icarus_lowerable asp_solver witness still models the pre-#8980 spec (Vec<Clause>) #10450

Boundary

Touches only bootstrap/tests/icarus_lowerable.rs (the expected-signature table of lowerability_models_keep_real_source_signatures) and proofs/lean4/Trinity/IcarusLowerable/Completeness.lean (the ar_asp_solver_env / ar_asp_solver_module model). Not the spec, not the emitter: both are right.

Scenarios

• Master test-ratchet is red on every open PR since run d31bccd: lowerability_models_keep_real_source_signatures panics with "source signature changed; reassess the witness: pub struct Program { pub clauses: Vec, pub constraints: Vec, }".
• Cause: seals: verdict-blocked specs compile and seal; 11 refused specs fixed, 30 blocked ones listed (Refs #8314) #10370 (b2fbb75) rewrote specs/ar/asp_solver.t27 so it compiles (specs/ml tests never run: test-report BLOCKED on 50 of 61 specs; use resolution depends on how the spec path is spelled #8980): [Clause] / [AnswerSet] became fixed arrays plus counts, and solve now returns SolveResult. The test still expected the old Vec<Clause> output and the old Lean model.
• The module is still not Icarus-lowerable (t27c icarus-lowerable says not_lowerable) but for a different reason: string fields in Literal, reached from Program through Clause.

Requirements

• The expected signatures in the test are the real t27c gen-rust output for the current spec (Literal, Program, solve).
• The Lean model carries the real fixed-array sizes and the string fields, so ar_asp_solver_lowerable = false is true for the reason the Rust classifier gives, not for a stale one.
• The test is not added to any ratchet baseline.

Criteria

• The test lowerability_models_keep_real_source_signatures passes (run on the lab).
• corpus_classifier_matches_lean_completeness still passes; Lean builds with ar_asp_solver_lowerable = false.
• test-ratchet is green on the PR.

Requirements

FR-001: The test lowerability_models_keep_real_source_signatures in bootstrap/tests/icarus_lowerable.rs MUST expect the current t27c gen-rust output for Literal, Program, and solve from specs/ar/asp_solver.t27.

FR-002: The Lean model ar_asp_solver_env / ar_asp_solver_module in proofs/lean4/Trinity/IcarusLowerable/Completeness.lean MUST carry the real fixed-array sizes and string fields from the current spec so that ar_asp_solver_lowerable = false reflects the Rust classifier's actual reason (string fields in Literal reachable from Program through Clause).

FR-003: The test lowerability_models_keep_real_source_signatures MUST NOT be added to any ratchet baseline.

Success Criteria

• cargo test -p bootstrap lowerability_models_keep_real_source_signatures exits 0
• cargo test -p bootstrap corpus_classifier_matches_lean_completeness exits 0
• lake build in proofs/lean4 exits 0 with ar_asp_solver_lowerable = false
• ./test-ratchet exits 0 on the PR
• Updated files: bootstrap/tests/icarus_lowerable.rs, proofs/lean4/Trinity/IcarusLowerable/Completeness.lean