Add an upstream Lean Std list-model bridge and simp_to_model registration for Const.mergeWith, then replace Iris's bespoke TreeMap fold proof with a direct tactic proof.

Progress

The paired Lean/Iris refactor is staged and passes a fail-closed structural checker. A negative control confirmed that stock-native overlay replay cannot validate the changed tactic. Native attempts had not falsified the proof; they failed because Stage1 retained GCC while Lean expected a Clang-compatible target-triple query. A corrected checkpointed job was submitted, but queued compute is not counted as validation.

Strategy and discriminator

upstream model bridge plus native tactic replay

Model Const.mergeWith as a distinct-key-preserving list fold, register that model transformation with simp_to_model, and test the resulting imported metaprogram using a freshly built native Lean runtime.

Hypothesis: Pinned Lean v4.32.0 with the proposed Const.mergeWith model bridge will make simp_to_model close the unchanged Iris getElem?_mergeWith' theorem without a private fold lemma.

Test: Build patched Lean Stage1 natively, compile experiments/SimpToModelMergeWith.lean, then run check_upstream_bridge.py with that executable before attempting the full Iris build.

Rationale

The exact source delta now matches issue #127's intended proof shape and removes the bespoke Iris helpers, but the verification contract explicitly requires focused and full builds. Without a completed native receipt, promotion to candidate would be premature.

Claims requiring scrutiny

The Iris patch preserves the textual header and @[simp] attribute of getElem?_mergeWith'.
The Iris patch removes Option.pairMerge, Option.insertOrMerge, get?_foldl_alter_impl_sigma, getElem?_foldl_alter, and getElem?_mergeWith_eq_foldl.
The proposed Lean bridge supplies a Const.mergeWith list model, permutation and distinct-key lemmas, a pointwise getValue? theorem, and simp_to_model registrations.
A stock Lean v4.32.0 native runtime with patched overlay oleans does not execute the new imported tactic mapping.
No native or full-build success is claimed.

Evidence and scope

python3 scripts/check_upstream_bridge.py returned zero and native_compile_checked false.
.proof-experiments/20260723-063511-46f5ab recorded the passing static contract check.
.proof-experiments/20260723-063823-7333d5 recorded the expected stock-runtime negative control with return code 1.
git diff --check passed for the outer workspace and both nested repositories.
lab-iris-lean-127-simp-to-model-ec16acc0a37a was submitted with input script SHA-256 644fe18a4f542f24f67a69f50e97c799819851864144c2cf7774dd0433a73406.

Computational experiments

.proof-experiments/20260723-063511-46f5ab: static verification contract passed in 0.126 seconds.
.proof-experiments/20260723-063823-7333d5: stock-native overlay control exited 1 with the predicted untransformed mergeWith goal.
lab-iris-lean-127-simp-to-model-ec16acc0a37a: corrected native Stage1 experiment submitted; no result claimed while queued.

Independent checker

scripts/check_upstream_bridge.py independently compares the public theorem header to the pinned snapshot, checks required upstream registrations and removed bespoke helpers, rejects unsafe escapes, and invokes both the standalone fixture and focused Iris module when given a native Lean executable. Its static phase passed; native phase is pending.

Contribution gate

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome: progress
Public classification: progress

Cross-domain transfers tested

None recorded.

Established facts

Pinned Lean v4.32.0 has no pre-existing mergeWith entry in simp_to_model's modification map.
scripts/check_mergewith_blocker.py and the pinned Lean source snapshot. · Lean v4.32.0 DTreeMap internal tactic implementation. · computed
The paired source state satisfies the static theorem-header and escape-hatch contract.
.proof-experiments/20260723-063511-46f5ab. · The four patched source files at the hashes emitted by check_upstream_bridge.py. · computed
Stock-native overlay replay leaves the mergeWith model goal unchanged.
.proof-experiments/20260723-063823-7333d5. · Lean v4.32.0 stock executable with artifacts/lean-overlay. · computed

Ruled out in this epoch

Treating patched overlay oleans with the stock native executable as decisive validation.
The imported simp_to_model mergeWith registration on Lean v4.32.0. · The native runtime executed the old mapping and left mergeWith untransformed. · .proof-experiments/20260723-063823-7333d5 · A demonstrated Lean invocation mode that interprets the changed imported metaprogram rather than dispatching to the stock native implementation.
Promoting the Iris-local private fold lemma as resolution of issue #127.
The previously compiling Const.get?_foldl_merge fallback. · It retains an implementation-specific fold proof and therefore does not satisfy the requested robustness mechanism. · The prior fallback diff summarized in findings/epoch-003-native-stage1-discriminator.md. · Maintainer confirmation that a private implementation-model lemma satisfies issue #127 despite the absence of direct mergeWith automation.

Open leads

Complete native Stage1 validation of the upstream mergeWith bridge.
It is the only remaining test that directly distinguishes a valid tactic registration from the expected stock-runtime failure. · Review lab-iris-lean-127-simp-to-model-ec16acc0a37a and inspect its built Lean invocation and checker output. · high · open
If native registration fails, isolate whether the unresolved constant name is Const.mergeWith, its fully qualified implementation name, or mergeWith!.
A single trace of the transformed expression can select the exact modifyMap entry without another full Iris build. · Instrument a bounded local copy of simp_to_model's expression traversal in the standalone fixture. · normal · open

Continuation checkpoint

Objective: Obtain a hash-bound native completion receipt for the paired Lean/Iris patches.

First action: Inspect records/labs and lab-runs outputs for lab-iris-lean-127-simp-to-model-ec16acc0a37a; do not infer success from queue or progress state alone.

Stop condition: Promote only when native fixture, focused checker, and full Iris build all exit zero; redirect immediately if the native fixture retains the mergeWith model goal.

Next moves

Inspect the immutable completion record and content-addressed outputs for lab-iris-lean-127-simp-to-model-ec16acc0a37a.
If Stage1 succeeds, require check_upstream_bridge.py to report native_compile_checked true and verify the focused HeapInstances compile.
Run or confirm the full Iris Lake build only after the focused checks pass.
Regenerate a review-ready upstream Lean patch and downstream Iris patch from the validated source state.

Citations

Tool disclosure

GPT-5.6 Sol principal performed synthesis, source audit, patch reconciliation, experiment design, and review. A GPT-5.6 Terra source-discriminator delegate supplied advisory reconnaissance that Sol independently checked against source and artifacts. Lean 4.32.0, Lake, CMake, bundled Clang 22.1.4, Python 3.12 deterministic checkers, Git, shell diagnostics, the Proof Factory experiment recorder and checkpointed lab, and official GitHub sources were used. No model agreement was treated as validation.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 929.9s
Review state: not a result claim
Attempt ID: iris-lean-127-simp-to-model-20260723-064559-a6057e

Human review ledger

No human review recorded.