ThermalConductivityCert
plain-language theorem explainer
ThermalConductivityCert is a structure certifying exactly five thermal conductivity regimes on the phi-ladder, with adjacent conductivities in constant ratio phi and all values strictly positive. Materials physicists cite it when anchoring transport scaling to the Recognition Science phi-ladder in B9 depth derivations. The declaration is a bare structure definition that enumerates the three certification fields with no proof body.
Claim. A structure is defined by the conditions that the set of thermal conductivity regimes has cardinality 5, that the conductivity function satisfies $k(k+1)/k(k)=phi$ for every natural number $k$, and that $k(k)>0$ for every $k$, where $k(k)=phi^k$.
background
The module treats thermal conductivity regimes derived from the phi-ladder in B9 Materials Depth. It enumerates five regimes (ballistic, diffusive, phonon-dominated, electron-dominated, interface-limited) whose count equals configDim D=5. The conductivity function is introduced as $k(k)=phi^k$ on ladder rungs, using the golden ratio phi supplied by the quasicrystal module. An upstream annular-cost definition supplies a separate stiffness constant $k=(log phi)^2$, but the local ladder definition governs the ratio field.
proof idea
The structure is declared directly by its three fields. The cardinality field references the Fintype instance on the inductive regime type. The ratio and positivity fields are stated as universal quantifiers over the ladder function $k(k)=phi^k$. No lemmas or tactics appear inside the declaration.
why it matters
The structure supplies the three properties assembled into the explicit thermalConductivityCert instance later in the module. It formalizes the five-regime phi-ladder scaling required for B9 Materials Depth and aligns with the Recognition Science forcing chain in which phi is the self-similar fixed point (T6). It touches the eight-tick octave through the phi-ladder but does not address spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.