FoxDifferential/Completed/FiniteStage/Stage.lean

1import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Boundary

2import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Relators

3import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Rules

4import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Fundamental

5import FoxDifferential.Completed.FiniteStage.Stage.Fundamental.Formula

6import FoxDifferential.Completed.FiniteStage.Stage.KernelIdeal

7import FoxDifferential.Completed.FiniteStage.Stage.Naturality

8import FoxDifferential.Completed.FiniteStage.Stage.Semidirect

9import FoxDifferential.Completed.FiniteStage.Stage.Source

11/-

12PUBLIC_PAGE_SNAPSHOT

13generated_at: 2026-05-27T09:47:29+09:00

14lean_source: lean4/FoxDifferential/Completed/FiniteStage/Stage.lean

15translation_root: data/translation

16purpose: identifies the local data snapshot used to build pages/

17placement: after imports, never before imports

18-/

19/-!

20# Finite-stage completed Fox calculus

22Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

23-/