Pith. sign in
module module moderate

IndisputableMonolith.Physics.CasimirEffectFromRS

show as:
view Lean formalization →

Module packaging the RS-native Casimir factor 720 = 6! together with configuration counts and a certificate witness. Physicists tracing the parallel-plate vacuum-pressure lane in Recognition Science cite it for the combinatorial weight on boundary modes. Content is definitional setup plus thin certificates, not a long forcing proof.

claimThe Casimir combinatorial factor is $720 = 6!$, recorded as the RS-native weight on vacuum boundary modes, with an eight-tick specialization and a certificate packing the configuration count.

background

Recognition Science works in native units with fundamental tick $\tau_0 = 1$ and $\hbar = \varphi^{-5}$. The classical Casimir effect is the attractive pressure between conducting plates from restricted vacuum modes. This module sits in the physics layer and introduces the RS reading of that effect via a configuration type, a configuration count, and the bare factor $720 = 6!$.

Sibling names indicate casimir_factor, its eight-tick variant, and a CasimirCert witness. Upstream is only the Constants module (tick quantum and related RS units). The local goal is to fix the combinatorial prefactor before the pressure law and $\hbar$ substitution are bundled downstream.

proof idea

Definition and certificate module, not a deep tactic development. It fixes casimir_factor as $720 = 6!$, records the eight-tick specialization, exposes a configuration count, and packages a CasimirCert value. Argument structure is naming and thin equality/certificate assembly rather than a multi-step derivation from the forcing chain inside this file.

why it matters in Recognition Science

Direct import for CasimirEffectCertV2, the master certificate of the formal Casimir lane. That parent bundles the ideal parallel-plate pressure law, the RS boundary-mode cost reading, and the native $\hbar = \varphi^{-5}$ substitution. The factor $720 = 6!$ supplies the combinatorial weight those certificates need. It touches the eight-tick octave landmark (T7) via the specialized factor, keeping mode counting aligned with the discrete RS clock.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)