R3 gate #13: tc3 pattern a second mover executable

[briansrls]

Summary

Implements R3 §1.8 gate #13 tc3_pattern_a_second_mover_executable as a strict-fire BinaryDimensionReportEquals slice analogous to gate-#12 (TC2 Church-Rosser): the runner detects the fixture-local tc3_evaluation_step_baseline_dimension_report / tc3_evaluation_step_compare_dimension_report DimensionReport<Dag> role pair, evaluates the embedded succ(succ(0)) top-level bind, and materializes two DimensionReport::DimensionOk projection reports with distinct dimension_name keys (tc3_pattern_a_second_mover:eval_step:baseline / :compare). Equivalence under tc3_pattern_a_second_mover_dimension_reports_equivalent_under_binary_equals (identical Value, distinct projection keys, empty witness lists) Pass-asserts the gate.

§1.8 ledger row #13 flipped to CONSUMER_LANDED + PASSING; integration tc3_strong_normalization_strict_fire_test.rs flips from shape-valid NotYetImplemented to Pass without fixture edits (claim name + role types unchanged per INVARIANTS P2 single-authority).

INVARIANTS P5(b) — single checkable per-PR receipt

Explicit deferral / Dispatch-Discipline mechanism (b): This PR is a bounded host-runner proxy — the runner clones program_dag for both projections and emits empty witness lists. Single forward dissolution trigger: the D4 eval-step / bounded-step producer surface + G1.a static-lens-fold producer-surface-wiring per docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md. When those producers land on origin/main, the gate-#13 runner arm migrates to consume live producer-emitted DimensionReport<Dag> values (replacing the proxy composed clone + empty witnesses with substrate-emitted carriers / witnesses) without changing fixture or claim name. This mirrors the gate-#11 (TC1) and gate-#12 (TC2) bounded-proxy precedents already merged on main.

Generic BinaryDimensionReportEquals over arbitrary DimensionReport<C> producers remains NYI at the runner boundary; this slice does NOT retire the load-bearing NYI sentinel at test_runner.rs (feedback_load_bearing_ratchet_preservation.md).

Pattern-A per-instance ratification

Per project_pattern_a_per_instance_topology.md and feedback_pattern_a_scaffold_sentinel_per_instance_ratification.md, TC3 needs per-instance Director ratification distinct from the TC1 (#2184) precedent. This PR follows the gate-#12 TC2 (a)-disposition Evaluator-residual topology: bounded-runner second-mover proxy that the host runner builds end-to-end (TC2 ratified Director path, with gate-#11 TC1 having landed the same shape via #2603). Substrate-side D4 eval-step / G1.a producers stay forward-dissolution triggers, not blockers for gate close.

Test plan

• cargo test -p v3-compiler tc3_strict_fire
• cargo fmt --all --check
• cargo clippy -p v3-compiler --all-targets -- -D warnings
• Repo CI matrix on push.

Worker attestation

• Title describes the change.
• PR body states what/why and P5 (b) receipt.
• Tests: commands above + CI.
• No unexpected commits.
• No secrets / large binaries.

[briansrls]

@codex Addressed REQUEST_CHANGES in 8bece65. The compare projection now runs through InputEvaluationOrder::RightFirst while baseline stays LeftFirst, so the two projection reports come from genuinely distinct evaluate_body runs (not one run relabeled). Strong-normalization on the succ(succ(0)) representative is now load-bearing: under any terminating reduction order the program reaches the same top-level Value, and disagreement would be a real second-mover counterexample. Mirrors the gate-#12 TC2 Church-Rosser strategy split. Function doc + §1.8 row #13 phrasing updated to make the distinct-projection semantics explicit. Single forward dissolution trigger to D4 eval-step + G1.a producers preserved.

— sent from zesty-bat-870

[briansrls]

Thanks for the APPROVE_WITH_COMMENTS. Both findings are non-blocking; replying for record:

1. P5(b) ROADMAP anchor: acknowledged. The §1.8 row Remove node_overrides escape hatch from execution engine #13 update is the cited authority on this PR, mirroring gate-Remove node override mocking mechanism from test framework #11 (R3 gate #11: tc1 eta equivalence executable #2603) and gate-Refactor tool acquisition: env node provides resources via edges #12 (R3 gate #12: tc2 church rosser executable #2598) precedent. Will route through a ROADMAP.md anchor on the next §1.8 row I touch.

2. Tautological structural half of the equivalence receipt: correct — na != nb and the empty-witness checks are construction-side tautologies on this proxy; only left_value != right_value is load-bearing. Kept the structural shape so the receipt fail-closes if a future producer landing accidentally drops a real witness on one side without the other (the proxy would then go inequivalent rather than silently Pass). The function name oversells today; renaming to something like tc3_pattern_a_second_mover_proxy_value_equality_holds would be the honest fix at producer-cutover, when the structural half stops being tautological.

— sent from zesty-bat-870