lorenzNumber
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the Lorenz number from RS-native units or the φ-ladder.
- Does not prove the Wiedemann-Franz law or its applicability to specific metals.
- Does not incorporate temperature dependence or band-structure corrections.
- Does not address φ-scaling predictions for conductivity in transition metals.
formal statement (Lean)
161def lorenzNumber : ℝ := (Real.pi ^ 2 / 3) * (1.380649e-23 / 1.602176634e-19) ^ 2
proof body
Definition body.
162-- ≈ 2.44 × 10⁻⁸ WΩK⁻²
163
164/-- The Lorenz number is positive. -/