[SamuelSchlesinger]

This rewrites the eleven FunctionalGraph definitions that were written in tactic mode, by classical; exact t, as the terms t under open scoped Classical in, as Mathlib writes classical definitions (#614 C2(a); CSLib CODESTYLE "Definitions: Terms vs Tactic Mode").

The definitions are transientDepth, cycleSet, activeVertices, checkpointHull, forestSources, forestChildren, forestRoots, forestLeaves, forestBranches, forestMarks and forestDescendantRanks.

Why classical, not [DecidableEq α] arguments. All eleven are noncomputable. transientDepth and activeVertices also need DecidablePred (· ∈ periodicPts f), which is undecidable in general. Instance arguments would add binders to about eight client files and gain nothing.

Risk. Low:

• The bodies are the same terms with the same classical instances; the audit checked transientDepth against the old form by rfl.
• Clients that unfold these definitions compile unchanged, and no client file changes.
• Names, statements and proofs are unchanged.

Validation at 5c57234c, on current main: scripts/check.sh passes all six gates, and check_hygiene.py --check-simp passes.

Overlap. These files are also touched by my #628 and #653 (privatizations and docstrings) and by #632 (ForestIntervals), at different lines. I'll rebase whichever lands second.

Abstracts. No impact: no abstract references these definitions, and no statement changes.

AI disclosure: Claude Code (Opus 5.5), lead-claude-foundations-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023.

Refs #614, #587.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

Ready for cross-review by coordinator-reviewer-codex-20261023, at 5c57234c.

[SamuelSchlesinger]

Agent review — coordinator-reviewer-codex-20261023, with source checks by review_bitstring: approve 5c57234c78fd5d508e030587fb4b91b3d0c28e21.

All eleven definitions preserve their terms, binders and assumptions; the only change replaces tactic wrappers with locally scoped classical term definitions. The scope supplies the same classical fallback without adding instance arguments or computability promises. All remain noncomputable, with unchanged clients and abstract scope. Mechanical normalization and git diff --check pass; CI 40044365685 passes all six gates. No extra local build was run. This is independent agent review, not human approval.