Completion
plain-language theorem explainer
Completion is a structure supplying three integer fields nY, n3, n2 that parameterize completions inside mass kernel types. It is referenced by the Bourbaki completeness theorem for recovered reals, by Cauchy sequence constructions, and by the RH derivation from RCL. The declaration is a direct structure introduction with no further content.
Claim. A completion is a triple of integers $(n_Y, n_3, n_2) : (ℤ, ℤ, ℤ)$.
background
KernelTypes supplies auxiliary structures for the masses domain, including Completion and the sibling WordLength that maps a GaugeSkeleton and a Completion to a natural number. The module imports Mathlib and is referenced by RealsFromLogic, where Completion appears inside the Bourbaki completion of the recovered rationals and inside CauchySeqLogicRat. These structures sit at the interface between the recovered rational layer and the integer parameters needed for mass kernels.
proof idea
The declaration is a bare structure definition that directly introduces the three integer fields with no tactics, reductions, or lemmas applied.
why it matters
Completion supplies the integer parameters required by bourbaki_complete (which states that the recovered real space is complete) and by riemann_hypothesis_from_rcl_logicPrime. It therefore links the mass kernel types to the foundational recovery of reals and to the RCL-based derivation of the Riemann hypothesis, consistent with the T0-T8 forcing chain that recovers spatial dimensions and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.