[abiswas3]

Summary

The soundness proof now reconstructs a fixed advice tape from relaxed execution answers and proves untrustedAnswerLanguage_implies_inLanguage without sorryAx.
This integrates the accumulated soundness work since #26 and closes Layer 7, while retaining the three explicit outstanding obligations in the top-level soundness proof.

• Bring in the soundness layers, trace reconstruction interfaces, explicit assumptions and restrictions, and model updates pinned to Jolt commit 8bbb2357.
• Complete the stopping proof and construct replay rows, rebuilding the tape from each answer's low bytes and transferring execution, outputs, and spoil-assert conditions.
• Prove narrow advice-load adjacency and register-shift adjacency through one generic lift from expansion instruction lists to materialized bytecode rows.
• Share the instruction-frame theorem between tape growth and device relations, preserving the existing theorem statements and callers.
• Record proof obligations, declaration timings, and upstream model issues in methods/soundness.md and JoltConstraints/model_review.md.

This PR branch captures the audited feat/soundness commit abbe04532c57b7f18b1c6ec7562ad09fcc8e3956 so concurrent work can continue independently.
It reconciles main's squash of #26 and retains main's Lean CI action update to v1.6.2.
All Lean sources and Lake configuration are identical to the audited commit after reconciliation.

Verification

• Ran the full default build (JoltBytecode and JoltConstraints) with an isolated Lake build directory: 8,802 jobs passed.
• Did not modify LeanRV64D.lean or anything under LeanRV64D/ relative to main.
• git diff --check passed for the closing change and merge resolution.
• Audited the completed tape theorem and JoltInstance.soundness after building the integrated branch.

untrustedAnswerLanguage_implies_inLanguage depends only on propext, Classical.choice, Quot.sound, and the existing sys_enable_experimental_extensions axiom.
It has no sorryAx dependency.

The only sorryAx paths from JoltInstance.soundness pass through:

1. JoltInstance.soundness_execution_prefix_agreement.
2. JoltInstance.soundness_prover_accepts (C).
3. JoltInstance.soundness_spoil_asserts_pass (D).

The dependency traversal verified that all three are reachable and that excluding exactly those declarations removes sorryAx.
The existing branch_target_toNat bv_decide axiom remains recorded in the proof ledger; the tape closure adds no bv_decide use.
C remains intentionally assumed despite the documented trace-length counterexamples pending upstream resolution, so this PR does not claim a complete soundness proof.

Declaration timings include narrow_load_shape 40 ms and the migrated shift-pair proof 45 ms.
The shared frame theorem takes 878 ms, reducing execInstr_tapeGrowth from 580 to 6 ms and execInstr_rule_of_device_relation from 1,363 to 4 ms.
The complete tape check took 28.14 s during a concurrent build; the subsequent cached integrated build took 3.55 s, and its final axiom audit took 9.70 s.
The complete declaration timing tables are in methods/soundness.md.

AI assistance

Codex implemented and checked the tape reconstruction and shared proofs, ran the builds and axiom audits, and prepared this PR under Ari's direction.