FoxDifferential/Completed/FreeProC/RelationSubmoduleApproximation.lean

1import FoxDifferential.Completed.FreeProC.StageApproximation

2import FoxDifferential.Completed.FiniteStage.RelationSubmodule

3import FoxDifferential.Completed.FiniteStage.RelationIdealDerivative

5/-

6PUBLIC_PAGE_SNAPSHOT

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

8lean_source: lean4/FoxDifferential/Completed/FreeProC/RelationSubmoduleApproximation.lean

9translation_root: data/translation

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

11placement: after imports, never before imports

12-/

13/-!

14# Completed density from finite-stage relation-submodule exactness

16The finite-stage semidirect approximation theorem requires set-level coverage by source-kernel Fox

17derivatives. This file feeds it from a more structured finite-stage input:

19* module exactness: `ker ∂` is contained in the submodule generated by relation boundaries.

21The finite relation-boundary image is already stable under the target group algebra, so the

22generated submodule is an honest source-kernel derivative image.

23-/

25namespace FoxDifferential

27noncomputable section

29universe u v

31section CompletedFoxRelationSubmoduleExact

33open scoped Topology

35variable {ProC : ProCGroups.ProC.ProCGroupPredicate}

36variable {X H : Type u}

37variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

38variable [DecidableEq X]

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

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

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

43/-- Completed Fox density from finite-stage relation-submodule exactness. -/

44theorem boundaryCycles_subset_kernelClosure_of_relSubmoduleExact

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

46 {J : Type v}

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

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

49 (nstage : J → ℕ)

50 (π : ∀ j : J,

51 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

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

53 (hbasis :

54 HasLeftQuotientKernelNeighbourhoodBasis

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

56 (hboundary_stage :

57 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

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

59 ∀ j : J,

60 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

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

62 (hstage_module_exact :

63 ∀ j : J,

64 finiteFoxStageRelationBoundaryModuleExact

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

66 (hNstage_kernel :

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

68 (hkernel_word_projection :

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

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

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

72 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

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

74 refine

75 freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact

76 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage ?_

77 hNstage_kernel hkernel_word_projection

78 intro j

79 exact finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact

80 (X := X) (Nstage j) (nstage j) (hstage_module_exact j)

82/-- The same finite relation-submodule input places completed boundary cycles in the closed

83generated Fox graph target. -/

84theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relSubmodule_exact

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

86 {J : Type v}

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

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

89 (nstage : J → ℕ)

90 (π : ∀ j : J,

91 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

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

93 (hbasis :

94 HasLeftQuotientKernelNeighbourhoodBasis

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

96 (hboundary_stage :

97 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

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

99 ∀ j : J,

100 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

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

102 (hstage_module_exact :

103 ∀ j : J,

104 finiteFoxStageRelationBoundaryModuleExact

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

106 (hNstage_kernel :

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

108 (hkernel_word_projection :

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

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

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

112 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

113 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

114 (ProC := ProC) φ : Subgroup

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

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

117 exact

118 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

119 (ProC := ProC) φ

120 (boundaryCycles_subset_kernelClosure_of_relSubmoduleExact

121 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage

122 hstage_module_exact hNstage_kernel hkernel_word_projection)

123

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

125/-- Completed Fox density from the source-boundary relation-ideal reduction at every finite stage.

126

127This is the next attack route below relation-submodule exactness: instead of assuming finite

128module exactness directly, it suffices to prove that source-coordinate lifts whose source boundary

129lies in the explicit relation augmentation ideal project to relation-boundary vectors. -/

130theorem boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction

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

132 {J : Type v}

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

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

135 (nstage : J → ℕ)

136 (π : ∀ j : J,

137 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

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

139 (hbasis :

140 HasLeftQuotientKernelNeighbourhoodBasis

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

142 (hboundary_stage :

143 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

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

145 ∀ j : J,

146 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

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

148 (hstage_reduce :

149 ∀ j : J,

150 finiteFoxStageSourceBoundaryRelationIdealReduction

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

152 (hNstage_kernel :

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

154 (hkernel_word_projection :

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

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

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

158 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

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

160 refine

161 boundaryCycles_subset_kernelClosure_of_relSubmoduleExact

162 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage ?_

163 hNstage_kernel hkernel_word_projection

164 intro j

165 exact finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction

166 (X := X) (Nstage j) (nstage j) (hstage_reduce j)

167

168/-- The source-boundary relation-ideal route also places completed boundary cycles inside the

169closed-generated Fox graph target. -/

170theorem boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction

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

172 {J : Type v}

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

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

175 (nstage : J → ℕ)

176 (π : ∀ j : J,

177 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

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

179 (hbasis :

180 HasLeftQuotientKernelNeighbourhoodBasis

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

182 (hboundary_stage :

183 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

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

185 ∀ j : J,

186 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

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

188 (hstage_reduce :

189 ∀ j : J,

190 finiteFoxStageSourceBoundaryRelationIdealReduction

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

192 (hNstage_kernel :

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

194 (hkernel_word_projection :

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

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

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

198 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

199 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

200 (ProC := ProC) φ : Subgroup

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

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

203 exact

204 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

205 (ProC := ProC) φ

206 (boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction

207 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage

208 hstage_reduce hNstage_kernel hkernel_word_projection)

209

210

211

212section

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

214/-- Completed Fox density from the finite-stage relation-ideal derivative theorem.

215

216The finite-stage source-boundary relation-ideal reduction is supplied by

217`RelationIdealDerivative.lean`. The remaining inputs are the completion and approximation data:

218the quotient-kernel neighbourhood basis, compatibility of completed boundary cycles with finite

219stages, and compatibility of honest kernel-word points with their finite-stage projections. -/

220theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv

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

222 {J : Type v}

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

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

225 (nstage : J → ℕ)

226 (π : ∀ j : J,

227 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

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

229 (hbasis :

230 HasLeftQuotientKernelNeighbourhoodBasis

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

232 (hboundary_stage :

233 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

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

235 ∀ j : J,

236 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

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

238 (hNstage_kernel :

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

240 (hkernel_word_projection :

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

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

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

244 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

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

246 refine

247 boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction

248 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage ?_

249 hNstage_kernel hkernel_word_projection

250 intro j

251 exact finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives

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

253

254end

255

256/-- Completed boundary cycles lie in the closed-generated Fox graph target using the finite-stage

257relation-ideal derivative theorem. -/

258theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relDeriv

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

260 {J : Type v}

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

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

263 (nstage : J → ℕ)

264 (π : ∀ j : J,

265 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

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

267 (hbasis :

268 HasLeftQuotientKernelNeighbourhoodBasis

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

270 (hboundary_stage :

271 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,

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

273 ∀ j : J,

274 π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet

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

276 (hNstage_kernel :

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

278 (hkernel_word_projection :

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

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

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

282 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

283 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

284 (ProC := ProC) φ : Subgroup

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

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

287 exact

288 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

289 (ProC := ProC) φ

290 (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv

291 (ProC := ProC) φ Nstage nstage π hbasis hboundary_stage

292 hNstage_kernel hkernel_word_projection)

293

294end CompletedFoxRelationSubmoduleExact

295

296end

297

298end FoxDifferential