Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.CoronalTemperatureFromJCost

show as:
view Lean formalization →

Module linking solar coronal temperatures to the Recognition Science J-cost. It defines a domain cost on temperature ratios, a canonical positive threshold, and a certificate bundle CoronalTempCert that packages the nonnegativity and threshold facts. Astrophysicists working the RS mass/temperature ladder would cite the certificate. Structure is mostly definitions plus short positivity lemmas over the imported Cost layer.

claimOn temperature (or scale) ratios $x > 0$, a domain cost $C(x)$ is built from the RS $J$-cost $J(x) = \frac{x+x^{-1}}{2}-1$. A canonical threshold $\theta > 0$ is fixed, and a certificate asserts $C \ge 0$ together with the threshold positivity used to mark coronal-temperature regimes in RS-native units.

background

Recognition Science forces the unique symmetric cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$) via the Recognition Composition Law and the T5 uniqueness step. The Cost import supplies that $J$ and its elementary inequalities; Constants supplies the RS tick and related native units.

This astrophysics module treats coronal heating as a cost-threshold phenomenon: when a temperature (or energy-scale) ratio crosses a canonical positive level built from $J$, the configuration is certified as coronal. Sibling names indicate a domain-restricted cost, its evaluation identity, nonnegativity, the threshold and its positivity, and a bundled certificate type with an inhabited instance.

The local setting is therefore not a full hydrodynamic corona model, but a thin RS interface: cost on ratios, threshold, certificate.

proof idea

Definition-heavy module. domainCost is assembled from the imported $J$-cost on the relevant ratio; domainCost_at_eq and domainCost_nonneg are short algebraic or inequality wrappers over Cost. canonicalThreshold is a closed-form positive constant; canonicalThreshold_pos discharges positivity. CoronalTempCert packages these facts; cert and cert_inhabited supply a concrete inhabited certificate. No deep tactic developments beyond positivity and rewriting.

why it matters in Recognition Science

Places coronal temperature inside the same $J$-cost ledger that drives the forcing chain (T5 $J$-uniqueness, T6 $\phi$, mass ladder). Downstream graph is empty here, so the module is a leaf interface: it exposes CoronalTempCert for later solar-physics or ledger-audit developments rather than feeding a named parent theorem in-tree. It ties the phenomenological corona temperature scale to RS-native cost and threshold language instead of an ad hoc Kelvin fit, keeping astrophysical claims auditable against Cost and Constants.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)