FoxDifferential/Completed/FreeProC/StageApproximation.lean

1import FoxDifferential.Completed.FreeProC.Density

2import FoxDifferential.Completed.FiniteStage.SemidirectCycles

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/FoxDifferential/Completed/FreeProC/StageApproximation.lean

8translation_root: data/translation

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

10placement: after imports, never before imports

11-/

12/-!

13# Finite-stage approximation routes for completed Fox density

15This file adds the library layer between finite-stage Fox exactness and the completed density

16statement. It separates three ingredients:

18* quotient kernels form a neighbourhood basis in the completed semidirect product;

19* completed boundary cycles project to finite-stage boundary cycles;

20* finite-stage boundary cycles are covered by finite-stage relation-word cycles.

22The last theorem in this file is the intended bridge from the finite theorem

23`ker ∂ = im D` at every finite stage to the completed closure statement.

24-/

26namespace FoxDifferential

28noncomputable section

30universe u v

32section GenericStageExactClosureAPI

34variable {Y : Type u} [Group Y] [TopologicalSpace Y]

35variable {S T : Set Y}

37/-- Quotient-kernel density from exact finite-stage images.

39For each quotient stage `j`, let `Tstage j` be the image condition satisfied by points of `T`,

40and let `Sstage j` be the finite-stage image of algebraic approximants from `S`. If every

41`Tstage` point is in `Sstage`, and every `Sstage` point lifts to an actual point of `S`, then

42`T` is contained in the closure of `S`. -/

43theorem subset_closure_of_quotientKernel_stage_exact

44 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]

45 (π : ∀ j : J, Y →* Q j)

46 (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)

47 (Sstage Tstage : ∀ j : J, Set (Q j))

48 (hTstage : ∀ y : Y, y ∈ T → ∀ j : J, π j y ∈ Tstage j)

49 (hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)

50 (hlift_stage : ∀ j : J, ∀ q : Q j, q ∈ Sstage j →

51 ∃ s : Y, s ∈ S ∧ π j s = q) :

52 T ⊆ closure S := by

53 refine subset_closure_of_quotientKernel_approximation π hbasis ?_

54 intro y hy j

55 exact hlift_stage j (π j y) (hstage_exact j (hTstage y hy j))

57end GenericStageExactClosureAPI

59section CompletedFoxStageExact

61open scoped Topology

63variable {ProC : ProCGroups.ProC.ProCGroupPredicate}

64variable {X H : Type u}

65variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

66variable [DecidableEq X]

67variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]

68variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]

70omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in

71/-- Completed Fox density from exactness of arbitrary quotient-stage images.

73This is the general completed semidirect bridge: choose quotient maps out of the completed

74semidirect product, prove that boundary cycles land in the chosen finite-stage `Tstage`, prove

75finite-stage exactness `Tstage ⊆ Sstage`, and lift every `Sstage` point to an actual kernel word.

76-/

77theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stage_exact

78 [Fintype X] (φ : X → H)

79 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]

80 (π : ∀ j : J,

81 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →* Q j)

82 (hbasis :

83 HasLeftQuotientKernelNeighbourhoodBasis

84 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)

85 (Sstage Tstage : ∀ j : J, Set (Q j))

86 (hboundary_stage :

87 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

88 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →

89 ∀ j : J, π j y ∈ Tstage j)

90 (hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)

91 (hlift_stage :

92 ∀ j : J, ∀ q : Q j, q ∈ Sstage j →

93 ∃ w : FreeGroup X,

94 FreeGroup.lift φ w = 1 ∧

95 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) = q) :

96 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

97 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by

98 refine subset_closure_of_quotientKernel_stage_exact

99 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

100 (S := freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)

101 (T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)

102 π hbasis Sstage Tstage hboundary_stage hstage_exact ?_

103 intro j q hq

104 rcases hlift_stage j q hq with ⟨w, hw, hπw⟩

105 refine ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w, ?_, hπw⟩

106 exact freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet

107 (ProC := ProC) φ hw

108

109omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in

110/-- Completed Fox density from finite semidirect Fox exactness at every quotient stage.

111

112Here the finite-stage `Tstage` is the set of finite semidirect boundary cycles and the finite-stage

113`Sstage` is the set of honest kernel-word derivative points. The hypotheses that remain are the

114actual comparison data between completed stages and finite Fox stages. -/

115theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact

116 [Fintype X] (φ : X → H)

117 {J : Type v}

118 (Nstage : J → Subgroup (FreeGroup X))

119 [∀ j, (Nstage j).Normal]

120 (nstage : J → ℕ)

121 (π : ∀ j : J,

122 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

123 FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))

124 (hbasis :

125 HasLeftQuotientKernelNeighbourhoodBasis

126 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)

127 (hboundary_stage :

128 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

129 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →

130 ∀ j : J,

131 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

132 (X := X) (Nstage j) (nstage j))

133 (hstage_exact :

134 ∀ j : J,

135 finiteFoxStageBoundaryCyclesCoveredBySourceKernel

136 (X := X) (Nstage j) (nstage j))

137 (hNstage_kernel :

138 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)

139 (hkernel_word_projection :

140 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →

141 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =

142 finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :

143 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

144 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by

145 refine

146 freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stage_exact

147 (ProC := ProC) φ π hbasis

148 (fun j => finiteFoxStageSemidirectKernelWordDerivativeSet

149 (X := X) (Nstage j) (nstage j))

150 (fun j => finiteFoxStageSemidirectBoundaryCycleSet

151 (X := X) (Nstage j) (nstage j))

152 hboundary_stage ?_ ?_

153 · intro j

154 exact

155 (finiteFoxStageSemidirectBoundaryCyclesCoveredByKernelWords_iff

156 (X := X) (Nstage j) (nstage j)).2 (hstage_exact j)

157 · intro j q hq

158 rcases hq with ⟨w, hwN, hpoint⟩

159 refine ⟨w, hNstage_kernel j hwN, ?_⟩

160 calc

161 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w)

162 = finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w :=

163 hkernel_word_projection j w hwN

164 _ = q := hpoint

165

166omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in

167/-- Completed Fox graph-word density from finite semidirect Fox exactness at every quotient stage.

168

169This is the finite-quotient form that does not require words in the finite relation subgroup

170`Nstage j` to be genuine kernel words for `φ`. A word `w ∈ Nstage j` only has to project to the

171trivial right coordinate at the `j`-th finite stage; the completed approximant remains the honest

172graph point `(D w, φ(w))`. -/

173theorem freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_exact

174 [Fintype X] (φ : X → H)

175 {J : Type v}

176 (Nstage : J → Subgroup (FreeGroup X))

177 [∀ j, (Nstage j).Normal]

178 (nstage : J → ℕ)

179 (π : ∀ j : J,

180 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

181 FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))

182 (hbasis :

183 HasLeftQuotientKernelNeighbourhoodBasis

184 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)

185 (hboundary_stage :

186 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

187 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →

188 ∀ j : J,

189 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

190 (X := X) (Nstage j) (nstage j))

191 (hstage_exact :

192 ∀ j : J,

193 finiteFoxStageBoundaryCyclesCoveredBySourceKernel

194 (X := X) (Nstage j) (nstage j))

195 (hgraph_word_projection :

196 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →

197 π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w) =

198 finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :

199 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

200 closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ) := by

201 refine subset_closure_of_quotientKernel_stage_exact

202 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

203 (S := freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ)

204 (T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)

205 π hbasis

206 (fun j => finiteFoxStageSemidirectKernelWordDerivativeSet

207 (X := X) (Nstage j) (nstage j))

208 (fun j => finiteFoxStageSemidirectBoundaryCycleSet

209 (X := X) (Nstage j) (nstage j))

210 hboundary_stage ?_ ?_

211 · intro j

212 exact

213 (finiteFoxStageSemidirectBoundaryCyclesCoveredByKernelWords_iff

214 (X := X) (Nstage j) (nstage j)).2 (hstage_exact j)

215 · intro j q hq

216 rcases hq with ⟨w, hwN, hpoint⟩

217 refine ⟨freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w, ?_, ?_⟩

218 · exact ⟨w, rfl⟩

219 · calc

220 π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w)

221 = finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w :=

222 hgraph_word_projection j w hwN

223 _ = q := hpoint

224

225/-- Finite-stage semidirect exactness places every completed boundary cycle in the closed

226generated Fox graph target without assuming finite relation words are genuine kernel words. -/

227theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_graphWord_semi_exact

228 [Fintype X] (φ : X → H)

229 {J : Type v}

230 (Nstage : J → Subgroup (FreeGroup X))

231 [∀ j, (Nstage j).Normal]

232 (nstage : J → ℕ)

233 (π : ∀ j : J,

234 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

235 FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))

236 (hbasis :

237 HasLeftQuotientKernelNeighbourhoodBasis

238 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)

239 (hboundary_stage :

240 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

241 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →

242 ∀ j : J,

243 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

244 (X := X) (Nstage j) (nstage j))

245 (hstage_exact :

246 ∀ j : J,

247 finiteFoxStageBoundaryCyclesCoveredBySourceKernel

248 (X := X) (Nstage j) (nstage j))

249 (hgraph_word_projection :

250 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →

251 π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w) =

252 finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :

253 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

254 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

255 (ProC := ProC) φ : Subgroup

256 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set

257 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by

258 exact

259 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density

260 (ProC := ProC) φ

261 (freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_exact

262 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage hstage_exact

263 hgraph_word_projection)

264

265/-- The finite-stage semidirect exactness route also places every completed boundary cycle in the

266closed generated Fox graph target. -/

267theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_semi_exact

268 [Fintype X] (φ : X → H)

269 {J : Type v}

270 (Nstage : J → Subgroup (FreeGroup X))

271 [∀ j, (Nstage j).Normal]

272 (nstage : J → ℕ)

273 (π : ∀ j : J,

274 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

275 FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))

276 (hbasis :

277 HasLeftQuotientKernelNeighbourhoodBasis

278 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)

279 (hboundary_stage :

280 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

281 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →

282 ∀ j : J,

283 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

284 (X := X) (Nstage j) (nstage j))

285 (hstage_exact :

286 ∀ j : J,

287 finiteFoxStageBoundaryCyclesCoveredBySourceKernel

288 (X := X) (Nstage j) (nstage j))

289 (hNstage_kernel :

290 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)

291 (hkernel_word_projection :

292 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →

293 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =

294 finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :

295 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

296 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

297 (ProC := ProC) φ : Subgroup

298 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set

299 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by

300 exact

301 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

302 (ProC := ProC) φ

303 (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact

304 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage hstage_exact

305 hNstage_kernel hkernel_word_projection)

306

307end CompletedFoxStageExact

308

309end

310

311end FoxDifferential