lorenzNumber
plain-language theorem explainer
lorenzNumber supplies the numerical value of the Lorenz number L = (π²/3)(k_B/e)² ≈ 2.44 × 10^{-8} W Ω K^{-2} derived from fundamental constants. Researchers in condensed matter physics cite it when linking thermal and electrical conductivities in metallic systems under the Recognition Science metallic bonding model. The definition proceeds by direct substitution of Boltzmann's constant and the elementary charge into the classical Wiedemann-Franz expression.
Claim. The Lorenz number is $L = (π²/3) (k_B / e)^2$, where $k_B = 1.380649 × 10^{-23}$ J/K is Boltzmann's constant and $e = 1.602176634 × 10^{-19}$ C is the elementary charge.
background
The MetallicBond module models metallic bonding through electron delocalization across a lattice to minimize recognition cost (J-cost) while maintaining 8-tick coherence and φ-related scaling in conductivity. The Wiedemann-Franz law states that thermal conductivity κ and electrical conductivity σ are related by L = κ/(σ T), with L the Lorenz number. This definition embeds the standard numerical value using constants imported from the module's dependencies on empirical programs and simplicial ledger structures.
proof idea
The definition is a direct one-line assignment of the expression (Real.pi ^ 2 / 3) * (1.380649e-23 / 1.602176634e-19) ^ 2. It functions as a constant wrapper that supplies the value for the downstream positivity proof without additional lemmas or tactics.
why it matters
This definition feeds the theorem lorenz_positive, which establishes L > 0 via direct positivity of the factors. It fills the CH-011 metallic bonding derivation by supplying the transport constant that connects free-electron density to measurable conductivities. The placement aligns with the framework's use of 8-tick octave and delocalized states, though the value remains tied to empirical constants rather than pure φ-ladder derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.