Pith. sign in
module module moderate

IndisputableMonolith.Physics.HeatCapacityAnomalyFromJCost

show as:
view Lean formalization →

Module packages a J-cost model of a heat-capacity anomaly: a nonnegative domain cost, a positive canonical threshold, and an inhabited certificate that the anomaly sits above that threshold. Condensed-matter and RS auditors cite it when linking thermodynamic jumps to the recognition cost. Structure is definitional plus elementary positivity lemmas, not a deep derivation.

claimDefine a domain cost $C$ built from the recognition cost $J$, prove $C\ge 0$ and $C$ agrees with $J$ on the evaluation point, fix a positive canonical threshold $\theta>0$, and package an inhabited certificate that the heat-capacity anomaly exceeds $\theta$.

background

Recognition Science measures mismatch by the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law and the T5 uniqueness step. Thermodynamic anomalies are read as excess cost relative to a reference scale set by RS constants ($\tau_0=1$ tick, $\phi$-ladder units).

This physics module sits on Constants and Cost. It introduces a domain-level cost functional, records that the functional is nonnegative and matches $J$ at the evaluation point, and fixes a positive canonical threshold against which an anomaly is certified. No continuum statistical mechanics is assumed; the objects are pure cost comparisons in RS-native units.

proof idea

Definition module with thin lemmas. Domain cost is introduced as a wrapper around $J$; equality-at-point and nonnegativity are immediate from the corresponding $J$ facts. The canonical threshold is a positive constant (positivity is a one-line arithmetic check). The certificate type bundles the inequality "anomaly cost $\ge$ threshold"; inhabitation is by direct construction from those lemmas. No analytic estimates or series expansions appear.

why it matters in Recognition Science

Gives a named, checkable bridge from the abstract $J$-cost to a concrete condensed-matter observable (heat-capacity anomaly) inside the RS physics layer. Downstream consumers would be higher-level anomaly or materials theorems that need a certified excess-cost witness; the present graph lists no used_by edges yet, so the module is a leaf certificate factory. It does not touch the forcing chain T0–T8, the eight-tick octave, or the $\alpha$ band; it only reuses $J$ and RS constants. Open question it prepares: whether measured heat-capacity jumps sit in the predicted threshold window once experimental units are converted to the $\phi$-ladder.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)