lorenz_positive
plain-language theorem explainer
The declaration proves the Lorenz number exceeds zero. Researchers deriving transport coefficients in metallic systems under Recognition Science would reference this positivity result to ensure physical consistency in conductivity ratios. The proof reduces the claim to the explicit definition of lorenzNumber and applies standard positivity preservation rules for products and quotients of positive reals.
Claim. The Lorenz number $L = (π^2 / 3) (k_B / e)^2$ satisfies $L > 0$, where $k_B = 1.380649 × 10^{-23}$ J/K and $e = 1.602176634 × 10^{-19}$ C.
background
In the metallic bonding module the Lorenz number arises from the Wiedemann-Franz law relating thermal conductivity κ to electrical conductivity σ via L = κ/(σT). The definition is L := (π²/3) (k_B/e)² with the given numerical constants for k_B and e. This sits within the RS mechanism for metallic states, where delocalized electrons minimize J-cost through 8-tick coherence and φ-scaling of conductivities. The upstream result supplies the explicit real-valued definition of lorenzNumber as (Real.pi ^ 2 / 3) * (1.380649e-23 / 1.602176634e-19) ^ 2, noted as approximately 2.44 × 10⁻⁸ WΩK⁻² and derivable from fundamental constants.
proof idea
The proof is a direct term-mode reduction. It first simplifies the goal using the definition of lorenzNumber, then applies mul_pos to split the product into two positive factors. The first factor is shown positive by div_pos applied to sq_pos_of_pos of Real.pi_pos and a norm_num positive denominator. The second factor is shown positive by sq_pos_of_pos on a quotient whose positivity follows from norm_num on the constants.
why it matters
This result secures the sign of the Lorenz number for applications in the metallic bonding derivation (CH-011). It supports the prediction that electrical conductivity correlates with free electron density in the delocalized electron sea model. Within the broader framework it aligns with the 8-tick octave and φ-scaling for transport properties, though no direct downstream theorems yet invoke it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.