Pith. sign in
module module moderate

IndisputableMonolith.Thermodynamics.HeatTransferFromJCost

show as:
view Lean formalization →

This module defines heat transfer regimes, Nusselt numbers at rungs, and associated certificates derived from J-cost in Recognition Science. Researchers modeling convective processes on the phi-ladder would cite these when building RS-native thermodynamics. It is a definition module containing no theorems or proofs.

claimDefinitions of HeatTransferRegime (regimes for J-cost based transfer), regimeCount, nusseltAtRung : \mathbb{N} \to \mathbb{R} (Nusselt number at rung), nusseltRatio, HeatTransferCert, and heatTransferCert.

background

The module sits in the thermodynamics domain and imports Constants, whose sole documented object is the fundamental RS time quantum \tau_0 = 1 tick. It introduces sibling objects that translate J-cost into heat transfer quantities: regimes, rung-indexed Nusselt numbers, ratios, and a certificate type. No module-level doc-comment supplies further setting; the upstream import anchors all quantities to the RS-native tick.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the heat-transfer layer of Recognition Science thermodynamics and would feed any parent theorems on thermodynamic closure or energy transport. It has no listed downstream uses yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)