five_is_Dconfig
plain-language theorem explainer
The theorem equates the natural number 5 with Dconfig, the configuration dimension appearing in the RS cardinality spectrum. Cross-domain analysts cite this witness when confirming that spectrum members decompose into the listed primitives such as configDim 5 and gap45. The proof reduces immediately to reflexivity because Dconfig is defined to be exactly 5.
Claim. $5 = D_{config}$
background
The module collects witnesses for the RS cardinality spectrum {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, ...}. Each element is obtained by sums, products, or powers of the cube-generators {2, 3}, the configDim 5, and gap45. Dconfig is introduced as the definition Dconfig : ℕ := 5, supplying the base value for this spectrum member.
proof idea
The proof is a one-line term-mode application of reflexivity (rfl). It succeeds directly because the right-hand side is literally the constant 5 supplied by the upstream definition of Dconfig.
why it matters
This equality supplies the explicit witness that 5 belongs to the RS cardinality spectrum as the configuration dimension. It supports the module claim that every listed cardinality admits a decomposition into RS primitives. The result closes a basic structural check in the cross-domain spectrum and feeds no further downstream theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.