Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.PeriodicBlocks

show as:
view Lean formalization →

The PeriodicBlocks module defines shell scales and block capacities in Recognition Science chemistry such that shell scale equals E_coh times capacity at each n. Researchers extending RS primitives to atomic periodicity would cite these definitions. The module imports Constants and consists of three sibling definitions with the core identity stated directly and no proofs present.

claim$shell(n) = E_{coh} · capacity(n)$ for each integer n, where E_coh derives from RS constants and capacity is given by the block_capacity definition.

background

The module operates in the Chemistry domain of Recognition Science. It imports IndisputableMonolith.Constants, whose doc-comment states that the fundamental RS time quantum is τ₀ = 1 tick. The module introduces the sibling definitions block_capacity, shell, and blocks_holds that together encode the stated identity relating shell scales to capacities via cohesion energy at each level n.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the periodic blocks identity that supports derivations of chemical periodicity from RS primitives. It depends directly on the Constants module and positions the shell-capacity relation for use in higher-level chemistry results within the Recognition framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)