kappa_pos
plain-language theorem explainer
kappa_pos asserts that the conductivity function kappa(k) equals phi to the power k and remains strictly positive for every natural number k. Material modelers working on the five phi-ladder regimes cite it to guarantee positive transport coefficients before taking ratios or limits. The proof is a one-line wrapper that invokes the general fact that a positive base raised to a natural exponent stays positive.
Claim. For every natural number $k$, $0 < phi^k$ where $kappa(k) := phi^k$ denotes the thermal conductivity on the ladder.
background
The module treats thermal conductivity as a function on the phi-ladder with five regimes (ballistic through interface-limited) and D=5. kappa is defined directly as phi^k. The positivity statement is drawn from the gravity module, where kappa_rs expands to 8 * phi^5 and is shown positive by mul_pos and pow_pos, and from the annular-cost module where kappa equals (log phi)^2 and is shown positive via log_pos and nlinarith. The local setting is the derivation of adjacent-regime conductivity ratios from the same ladder.
proof idea
This is a one-line wrapper that applies pow_pos phi_pos k.
why it matters
The result supplies the kappa_pos field required by ContinuumBridgeCert, which certifies that J-cost stationarity on the simplicial ledger yields the Einstein equations with coupling 8 phi^5. It is also referenced by CubicFieldCurvatureCert and continuumFieldCurvatureCert to close positivity in the continuum limit. The declaration therefore anchors the positivity step in the T5-T8 forcing chain when thermal properties are lifted to the continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.