kappa_ratio
plain-language theorem explainer
The ratio of thermal conductivities on adjacent rungs of the phi-ladder equals phi. Materials modelers cite this when deriving the five canonical conductivity regimes from the Recognition Science ladder. The proof unfolds the exponential definition of kappa, invokes positivity of phi to the k, rewrites the division, applies the successor power rule, and finishes with ring simplification.
Claim. For each natural number $k$, the ratio of thermal conductivities on adjacent rungs of the phi-ladder satisfies $kapp(k+1)/kapp(k)=phi$, where $kapp(k):=phi^k$.
background
The module models thermal conductivity via five regimes on the phi-ladder (configDim D=5): ballistic, diffusive, phonon-dominated, electron-dominated, and interface-limited. The local definition kappa(k) := phi^k supplies the exponential scaling between rungs. This differs from the stiffness constant kappa := (log phi)^2 appearing in AnnularCost. The setting follows the Recognition Science forcing chain in which phi is the self-similar fixed point (T6).
proof idea
The term proof unfolds kappa to obtain phi^{k+1}/phi^k. It adds the hypothesis that phi^k is positive, rewrites the division via div_eq_iff, replaces the numerator with the successor power, and closes by ring.
why it matters
The theorem populates the phi_ratio field of ThermalConductivityCert, which certifies the five regimes. It supplies the adjacent-rung scaling required by the phi-ladder construction (T6) and the eight-tick octave (T7). The result feeds the downstream ClusterLensing kappa_ratio bound under RS parameter locks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.