[PerAlexandersson]

Draft, unverified by the integrator. Phase B of #1978, drafted by a Codex worker. The worker reports a passing full default build (11112 jobs) and guards. Still to do before merging: golfw/verify_lane.sh, i.e. strict runLinter against nolints.json, the coverage check and the catalog audit, plus my review of the code.

Recurrence spaces phase B report

B1: short-certificate replay

• Added rr_replay_lift: infers the lift data from the goal, applies
  liftDefect_eq_zero_of_lagDefect_eq_zero, and checks the concrete factor identity with
  decide or polynomial normalization. The source recurrence and the bundled k seeds are
  supplied as proof terms.
• Added rr_replay_source: replays the converse certificate from the lift, the source seed,
  and affineIndex ... (n + k) ≠ 0; its factor identity is normalized automatically.
• Added the internal rr_replay_factor normalizer. Its terminal done makes altered factors
  fail rather than leave residual goals.
• Files: RealRooted/Tactic/Recurrence.lean and
  RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean.

B2: exceptional indices

• Added liftDefect_eq_zero_from_of_lagDefect_eq_zero_from: a source recurrence from n₀
  plus the k seeds in [n₀, n₀ + k) proves the lift from n₀.
• Added lagDefect_eq_zero_from_of_liftDefect_eq_zero_from_of_exceptional: a lift from n₀
  plus a source seed at n₀ and an extra source seed after each zero affine leader proves
  the source recurrence from n₀.
• Added lagDefect_eq_zero_from_of_liftDefect_eq_zero_from: the specialization with no zero
  affine leaders.
• Added rr_replay_lift_from and rr_replay_source_from for the tail and exceptional-leader
  theorems. These variants take the already checked factor equality explicitly.
• File: RealRooted/RecurrenceSpace/Defect.lean; tactic regressions are in the A049325 example
  module.

B3: row-tactic adapter

• Added derivativeRecurrence_of_liftDefect_eq_zero: for a lift whose leader is the nonzero
  scalar polynomial C (delta n), produces the normalized recurrence in the existing
  A * P' + B * P convention.
• Added rr_lift_recurrence, which applies that bridge while leaving degree, leading-sign,
  root-window propagation, root-sign, and base-row goals to existing theory/tactics.
• The acceptance module applies the adapter directly as the recurrence premise of
  derivativeRecurrence_interlaces_of_window; the same premise shape feeds
  derivativeRecurrence_interlaces_of_roots_mem_Icc and
  derivativeRecurrence_interlaces_of_roots_le.
• Files: RealRooted/RecurrenceSpace/Defect.lean, RealRooted/Tactic/Recurrence.lean.

B4: acceptance regressions

• A049325 now obtains its all-index lift with rr_replay_lift, replacing the manual theorem
  application and explicit factor-certificate argument.
• hermiteReplay_succ checks H[n+1] = 2X H[n] - H[n]' through
  rr_lift_recurrence.
• Added a generic root-window handoff regression, a shifted-origin replay, a regular converse,
  and an exceptional-leader converse.
• Added two fail_if_success regressions: one changes gamma from X to X + 1; the other
  supplies seeds for the corrupted derivative coefficient X * (X + 15).
• Regenerated RealRooted/Tactic/OEIS_COVERAGE.md; updated the two affected import budgets in
  scripts/import_architecture.json.

Nothing in B1--B4 was skipped. Later targets from issue #1978 outside this phase-B brief were
not attempted.

Verification

Focused target:

Build completed successfully (9152 jobs).
GUARD: exit=0 peak_anon_MB=0 peak_total_anon_MB=0 peak_rss_MB=0

Full default target:

Build completed successfully (11112 jobs).
GUARD: exit=0 peak_anon_MB=1505 peak_total_anon_MB=1505 peak_rss_MB=7859

./guards.sh:

check_import_architecture ok
check_example_namespaces ok
check_proof_status ok
check_root_imports ok
check_upstream_headers ok
ok: validated 106 curated catalog pages
lint-style rc=0

The generated coverage --check and git diff --check also passed.

🤖 Generated with Claude Code