FoxDifferential/Completed/FreeProC.lean

1import FoxDifferential.Completed.FreeProC.SemidirectLift

2import FoxDifferential.Completed.FreeProC.Uniqueness.Derivative

3import FoxDifferential.Completed.FreeProC.Uniqueness.Existence

4import FoxDifferential.Completed.FreeProC.Uniqueness.Lift

5import FoxDifferential.Completed.FreeProC.Uniqueness.Morphism

6import FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom

7import FoxDifferential.Completed.FreeProC.Density

8import FoxDifferential.Completed.FreeProC.StageApproximation

9import FoxDifferential.Completed.FreeProC.RelationSubmoduleApproximation

10import FoxDifferential.Completed.FreeProC.StageProjection

11import FoxDifferential.Completed.FreeProC.QuotientKernelBasis

12import FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis

13import FoxDifferential.Completed.FreeProC.PrimePowerStageProjection

14import FoxDifferential.Completed.FreeProC.BifilteredStageProjection

15import FoxDifferential.Completed.FreeProC.BifilteredSystemStageProjection

16import FoxDifferential.Completed.FreeProC.CoordinateStageProjection

17import FoxDifferential.Completed.FreeProC.BifilteredCoefficientStageProjection

18import FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection

19import FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageProjection

20import FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageRightProjection

21import FoxDifferential.Completed.FreeProC.FiniteQuotientStages

22import FoxDifferential.Completed.FreeProC.SemidirectKernelBasis

25PUBLIC_PAGE_SNAPSHOT

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

27lean_source: lean4/FoxDifferential/Completed/FreeProC.lean

28translation_root: data/translation

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

30placement: after imports, never before imports

32/-!

33# Free pro-C completed Fox calculus

35Free pro-C sources are treated through completed Fox derivatives, stage projections, density arguments, and semidirect lift formulas.