casimir_factor
plain-language theorem explainer
The identity 720 equals six factorial anchors the prefactor in the Casimir energy formula under Recognition Science scaling. Workers deriving vacuum forces between plates in RS-native units reference it when substituting hbar equal to phi to the minus five into the standard expression. The proof is a direct computational verification that succeeds without additional lemmas or hypotheses.
Claim. $720 = 6!$
background
The CasimirEffectFromRS module treats the attractive force between parallel conducting plates arising from quantum vacuum fluctuations. Standard QFT gives the energy per unit area as E = -π² ℏ c / (720 d⁴); RS replaces ℏ with φ^{-5} while keeping c = 1, so the numerical factor 720 remains the key coefficient. The module explicitly notes that 720 also equals 8 × 90, tying the identity to the eight-tick octave structure. The upstream tick definition supplies the fundamental time quantum τ₀ = 1 that underlies the discrete evolution periods used throughout the RS forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic evaluates both sides of the equality by direct computation of the factorial and confirms numerical identity without invoking any other lemmas.
why it matters
The theorem populates the factor_720 field inside the casimirCert definition, which also records the five canonical configurations and the separate 8-tick factor. It thereby supplies the concrete numerical anchor required for the Casimir energy formula in the RS framework, directly supporting the T7 eight-tick octave landmark. The result closes a small computational gap rather than leaving an open scaffolding question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.