research: [1618] map body-proof dependency graph

[Th0rgal]

References #1618.

This PR delivers Option A: a dependency map document at docs/research/1618-axiom-dependency-map.md.

Why this option:

• On current main, the branch state has already moved beyond the issue text: the non-core/non-terminal fallback is no longer a direct axiom call.
• GenericInduction.lean already contains supported_function_body_correct_from_exact_state_generic and the helper-aware wrapper.
• The highest-leverage blocker is therefore the exact theorem wiring: which theorem calls which branch, what hypotheses are passed, and what contract the generic replacement still has to preserve.

What the document covers:

• every in-repo call site of the core, terminal, and generic exact-state body theorems in Function.lean and GenericInduction.lean
• the caller theorem at each site
• the preconditions passed at each call
• which branch is being exercised
• what would change if the historical axiom slot were replaced by a proved theorem with the same signature

Notable finding:

• At commit e7435c67e59c70c882aab4106133fd80f8a47ba3, there is no remaining direct declaration or call site of supported_function_body_correct_from_exact_state on main; the generic-with-helpers theorem now occupies that fallback slot.

This is research-only. No existing .lean files were modified.

---

Note

Low Risk
Documentation-only change adding a research note; no production code, proofs, or build behavior is modified.

Overview
Adds a research document docs/research/1618-axiom-dependency-map.md that maps the current dependency/call graph around the historical supported_function_body_correct_from_exact_state axiom slot, documenting how supported_function_correct dispatches between core/terminal/generic theorems and what hypotheses/contracts each branch relies on.

^{Written by Cursor Bugbot for commit a6d0891. This will update automatically on new commits. Configure here.}