Pith. sign in
module module moderate

IndisputableMonolith.Physics.Gas_Constant_RS

show as:
view Lean formalization →

Defines the ideal-gas constant in Recognition Science units from a non-negative domain cost functional and a positive canonical threshold. Physicists matching RS thermodynamics to SI gas laws would cite GasConstRS and its certificate. The module is mostly definitional: cost non-negativity and threshold positivity discharge a small inhabited certificate.

claimIn RS-native units the gas constant is the value $R_{\mathrm{RS}}$ obtained from a domain cost $C$ (non-negative, with a fixed evaluation identity) and a positive canonical threshold $\theta_{\mathrm{can}}$. The module packages $R_{\mathrm{RS}}$ together with a certificate that these positivity and evaluation conditions hold.

background

Recognition Science works in units fixed by the fundamental tick $\tau_0=1$ (from Constants) and the J-cost calculus (from Cost). Thermodynamic constants must be expressed as dimensionless or tick-scaled combinations of those primitives rather than imported SI values.

This module introduces a domain cost functional on the relevant configuration space, records that the cost is non-negative and that evaluation at a distinguished point is well-defined, and fixes a positive canonical threshold. The gas constant in RS units is then the scalar assembled from that cost and threshold.

The local setting is pure definition-plus-certificate: no dynamical PDE or statistical-mechanics limit is proved here; the objects are the algebraic ingredients needed downstream when matching $PV=nRT$ style relations to RS ladder and tick structure.

proof idea

Definition module with light positivity lemmas. domainCost and canonicalThreshold are introduced as defs; domainCost_nonneg and canonicalThreshold_pos are short non-negativity/positivity facts; domainCost_at_eq records the evaluation identity. GasConstRS assembles the scalar. cert and cert_inhabited package those facts into an inhabited certificate record. No deep tactic proof or forcing-chain argument appears.

why it matters in Recognition Science

Places the ideal-gas constant on the same RS-native footing as $c=1$, $\hbar=\varphi^{-5}$, and $G=\varphi^5/\pi$. Downstream thermodynamics or equation-of-state developments can cite GasConstRS instead of an external SI import. The module currently has no recorded used-by edges in the mirror graph, so it is a leaf definition block awaiting consumers in broader physics layers. It does not itself touch T0–T8, RCL, or the mass ladder; it only supplies a constant once those structures are already fixed.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)