casimirConfigCount
plain-language theorem explainer
The theorem establishes that the inductive type enumerating Casimir configurations has cardinality exactly five. Researchers deriving the vacuum energy prefactor in Recognition Science QFT models would cite this count when assembling the certification of the 720 factor. The proof is a one-line decide tactic that exhausts the finite type constructors.
Claim. The set of Casimir configurations has cardinality five: $|C| = 5$, where $C$ consists of the five geometries parallel plates, sphere-plate, cylinder-plate, corrugated, and sphere-sphere.
background
The CasimirEffectFromRS module treats the Casimir effect as vacuum fluctuations between conducting surfaces, giving energy per unit area $E = -π²ℏc/(720 d⁴)$ with ℏ = φ^{-5} in RS units. CasimirConfig is defined as an inductive type whose five constructors are exactly the canonical geometries: parallelPlates, spherePlate, cylinderPlate, corrugated, sphereSphere; it derives Fintype so that cardinality is computable. The module notes that 720 = 6! and also equals 8 × 90, linking the configuration count to the eight-tick octave.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card CasimirConfig. Because CasimirConfig derives DecidableEq, Repr, BEq and Fintype, decide reduces the equality to a finite enumeration of the five constructors and confirms the cardinality is 5.
why it matters
This supplies the five_configs field inside casimirCert, which packages the full certification of the Casimir factors (720 and its 8-tick decomposition). It fills the module's explicit claim that configDim D = 5 and that 720 = Nat.factorial 6, anchoring the Recognition Science treatment of QFT depth to the T7 eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.