thermalConductivityCert
plain-language theorem explainer
The definition supplies a certificate asserting exactly five thermal conductivity regimes on the φ-ladder, with adjacent ratios fixed at φ and all κ values positive. Materials physicists working on phonon transport in quasicrystals cite it to anchor scaling relations across ballistic to interface-limited regimes. It assembles the certificate by direct field assignment from the regime cardinality theorem, the algebraic ratio identity, and the power positivity lemma.
Claim. Let κ(k) be the conductivity at rung k on the φ-ladder. The certificate requires exactly five regimes, κ(k+1)/κ(k) = φ for every k, and κ(k) > 0 for every k. The definition constructs the unique such certificate by assigning the regime count, the ratio identity, and the positivity property.
background
The module classifies thermal conductivity into five regimes on the φ-ladder: ballistic, diffusive, phonon-dominated, electron-dominated, and interface-limited. The structure encodes three requirements: the cardinality of the regime type is five, adjacent conductivities scale by the golden ratio φ, and every conductivity remains strictly positive. This construction sits inside the Recognition Science materials depth (B9), where conductivity inherits the self-similar scaling already fixed by the φ-ladder and the Recognition Composition Law.
proof idea
The definition is a direct structure constructor. It populates the five-regime field with the decide result on cardinality. The ratio field receives the algebraic identity obtained by rewriting the power ratio and applying ring normalization. The positivity field receives the theorem that any positive base raised to a natural-number exponent stays positive.
why it matters
The definition closes the certificate for the five-regime thermal model required by the φ-ladder in the materials sector. It supplies the concrete object that later derivations of transport coefficients can invoke without re-proving the scaling or positivity facts. No downstream theorems are recorded yet, but the construction directly supports the B9 depth claim that conductivity regimes are enumerated by configDim D = 5 and inherit the eight-tick octave periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.