[SamuelSchlesinger]

Part of #614 (Item C2: FunctionalGraph remainder after #661, announced on #587).

Summary

1. Complexity/Foundations/Combinatorics/FunctionalGraph.lean:
   • Adds transientDepth_eq_zero_of_mem_periodicPts and cycleLength_eq_minimalPeriod_of_mem_periodicPts (replacing 4 in-place re-derivations across Circuit/Boolean/Iteration).
   • Marks transientDepth_iterate @[simp].
2. Complexity/Foundations/Combinatorics/FunctionalGraph/Cycle.lean & HittingTime.lean:
   • Defines cycleSet via periodicOrbit: (periodicOrbit f (f^[transientDepth f x] x)).toFinset.
   • Simplifies mem_cycleSet_iff (exact Multiset.mem_toFinset) and marks mem_cycleSet_iff, cycleLength_iterate, cycleSet_iterate, canonicalCycle_iterate, and phase_iterate @[simp].
   • Moves iterate_eq_iterate_iff_modEq and transientDepth_le_canonicalTime from HittingTime.lean into Cycle.lean so both HittingTime.lean and Spectrum.lean reuse them directly.
3. Marks *_iterate and mem_* lemmas @[simp] across FunctionalGraph:
   • Projection.lean: cycleProjection_iterate
   • Active.lean: mem_activeVertices
   • CheckpointForest.lean: mem_checkpointHull, mem_forestSources, mem_forestChildren, mem_forestRoots, mem_forestLeaves, mem_forestBranches, mem_forestMarks
   • ForestIntervals.lean: mem_forestTrace, mem_forestPath, mem_forestDescendantRanks
4. Deduplicates Complexity/Foundations/Combinatorics/FunctionalGraph/Spectrum.lean:
   • Deletes cycleLength_le_card, card_add_mod_lt, and minimalPeriod_iterate_card.
   • Derives transientDepth_eq_zero_of_injective and cycleLength_eq_minimalPeriod_of_injective from transientDepth_eq_zero_of_mem_periodicPts and cycleLength_eq_minimalPeriod_of_mem_periodicPts.
   • Shortens iterate_eq_canonical_iff from 42 lines to 4 lines using canonicalTime_spec, iterate_eq_iterate_iff_modEq, and transientDepth_le_canonicalTime.
5. Renames forest_edges_merge to forest_edge_interior_inj:
   • Updates ForestSegments.lean, ForestNavigation.lean, and ComplexityTests/FunctionalGraph.lean so the theorem name reflects that compressed-edge interiors do not merge (x = y ∧ i = j).

Validation & Abstracts

• LEAN_NUM_THREADS=4 ./scripts/check.sh (all 6 gates passed)
• python3 scripts/check_hygiene.py --check-simp (all hygiene checks passed)
• python3 scripts/check_tidy_surface.py (2,021 statements in 423 modules, matching baseline)
• python3 scripts/build_abstracts.py --check (no impact on curated headline abstracts)

AI disclosure: Authored by worker-jetski-73aa4b5a (73aa4b5a-fa3d-4195-8024-b19f43bfa557).

[SamuelSchlesinger]

Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head 170683b9fac0e02df72ee417d1bf8c501dc00f6b, now confirmed GREEN.

The new cycleSet is the same finite set: periodicOrbit enumerates the iterates of the periodic entry up to its minimal period, and converting to a Finset gives the old image over the cycle length. Both old and new definitions remain noncomputable. Finite-type/universe assumptions and pointwise empty/singleton behavior are preserved. Periodic/injective helpers and the moved congruence lemmas retain their contracts; Spectrum’s canonical-time proof keeps the required transient lower bound and congruence orientation. The forest rename preserves its entire telescope/proof, with all clients updated and no alias.

The 245 retained public headers are unchanged; the two additions and three advertised unused convenience deletions match the intended scope. New simp rules reduce iterates or membership structure without an inverse rewrite cycle; they are on public theorems. Source credit, finite-layout/algorithm claims and headline abstracts are unchanged. No new executable or benchmark claim is made.

Actual merge base is 72a43356. Author’s local validation is retained. Updated after CI: exact-head CI40076277427, job120820196869, is SUCCESS across all six gates and the tidy statement ratchet. The live source head is unchanged. No fresh broad functional-graph audit or local full build is claimed. Ready at this exact head under the coordinator’s integration order.