test(applied): pin the Presentation depth-bound contract on both engines (#297)

[tsondru]

Closes #297. Taskmap G4-T1.

Premise probe (before briefing): the issue's production defect does not exist. normalize is for step in 0..rewrite_depth with no early exit other than the fixpoint return, so reaching the exhausted arm means exactly rewrite_depth passes ran — measured with an instrumented copy: 4 passes at depth 4, steps_taken 4. "8 iterations at depth 2" is a leaf count (A → A;A has 8 leaves after 3 passes), not loop passes. The reviewer independently confirmed no public-API observable can separate the exhausted-path steps_taken from the loop count. The issue's second claim was also wrong: presentation_structural_engine_returns_none_on_cyclic_overlap returned Some(true) and discarded it — A = B, B = A converges in one pass because both equations chain inside apply_user_equations.

Shipped (production diff 0; tests + CHANGELOG):

• eq_mod pinned at Ok(None) when a side hits the bound: Structural (A = A;A, depth 4) and CC (depth 0), each beside Some(true) / Some(false) on converging pairs of the same presentation.
• normalize pinned at depth 0 (converged false, steps 0, expr = input, with and without a matching equation) and at depths 1, 2 on A → A;A with expr written out (A;A, (A;A);(A;A)).
• The two vacuous A = B, B = A tests renamed to what they check and assert converged, expr, steps_taken (and eq_mod = Some(true)).

Falsification (-p catgraph-applied --no-fail-fast, impl + review, values in the messages):

perturbation (presentation/mod.rs)	red
Structural arm Ok(None) → Ok(Some(true))	…returns_none_only_when_a_side_hits_the_bound (Some(true) vs None)
CC arm → Ok(Some(false))	…cc_engine_returns_none…
steps_taken: rewrite_depth → + 1 / → 0	4 / 3 tests
loop 0.. → 0..=	no_iterations_at_depth_zero, steps_taken_tracks_depth… (expr pin)
apply_user_equations reversed	both paired-inverse tests (B vs A)
exhausted arm converged: true	4 tests
if after_smc == current	7 tests

Coverage fact: the Structural None, CC None, and 0..= perturbations are caught only by tests added here — zero pre-existing tests went red; 0..= is invisible to steps_taken (still 4) and caught only by the written-out expr. Nulls recorded: the depth-0 fixture cannot separate steps_taken: 0 from the bound (both 0); paired_inverse… cannot separate after_smc from after_user (both fixpoints on pass 1).

Reviews: executing adversarial (0 blocking / 1 important / 4 minor — CHANGELOG rationale, doc comments carrying mechanism, a stale stub, one wording) all applied except: an expr pin at depth 4 (a 16-leaf reassociated tree) — surfaced, not derived; the depth-1/2 expr pins carry the count cross-check. Delta review of the applied edits (1 important / 2 minor: my trimmed doc comments dropped stated values — normalize(B ⊗ Id(0)) = (B, 2 steps), two converged flags) → fix commit; every asserted value is now stated in its test's comment.

Gates: applied 45 binaries / 673 / 0 / 15; clippy -D warnings on default, all features, --no-default-features; fmt; version-refs.

🤖 Generated with Claude Code