blockFactor
plain-language theorem explainer
blockFactor supplies the dimensionless phi-powered multiplier for rail index n and block b as phi to the power of 2n plus the block offset. Modelers building fit-free periodic tables in Recognition Science cite it when constructing band energies on the phi-ladder. The definition is a direct arithmetic reduction that forms the exponent from twice n and the offset then applies real exponentiation to the constant phi.
Claim. For rail index $n$ and block $b$, the block factor equals $phi^{2n + delta(b)}$, where $delta$ is the offset map from the BlockOffsets class (default: $delta(s)=0$, $delta(p)=1$, $delta(d)=2$, $delta(f)=3$).
background
The Periodic Table Engine constructs the table from phi-tier rails with fixed offsets for the four blocks. Block is the inductive type with constructors s, p, d, f. BlockOffsets is the type class supplying offset : Block → ℤ, defaulting to the values 0, 1, 2, 3 respectively. This encodes the eight-tick octave structure without per-element parameters, as stated in the module documentation for the Noble Gas Closure Theorem (P0-A0).
proof idea
One-line definition that computes the exponent as twice the integer n plus the offset of b from the BlockOffsets instance, then raises the constant phi to that real power via Real.rpow.
why it matters
blockFactor is the direct input to bandMultiplier, which produces predicted band energies for atomic number Z. It supplies the phi-ladder scaling required by the Noble Gas Closure Theorem and instantiates the self-similar fixed point phi together with the eight-tick octave from the forcing chain. The definition closes the zero-parameter chemistry scaffold that forces noble-gas closures at the observed Z values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.