Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LogicRealConstants

show as:
view Lean formalization →

Defines Recognition Science fundamental constants on the recovered real line: golden ratio, tick, eight-tick octave, J-bit, coherence energy, ħ, G, Einstein κ, and α⁻¹. Physics and cost modules that stay inside LogicReal import these rather than Mathlib ℝ. Transport lemmas identify each constant with its ordinary real value through the LogicReal equivalence.

claimOn the recovered real line $\mathrm{LogicReal}\simeq\mathbb{R}$, the module fixes RS-native constants $\varphi_L$, tick $\tau_L$, octave period $2^3$, $J_{\mathrm{bit},L}$, $E_{\mathrm{coh},L}$, $\hbar_L=\varphi_L^{-5}$, $G_L=\varphi_L^5/\pi$, Einstein $\kappa_L$, and $\alpha^{-1}_L\in(137.030,137.039)$, each paired with a transport equality to its Mathlib real value.

background

Recognition Science works on a recovered real line LogicReal, equivalent to Mathlib's $\mathbb{R}$ by LogicReal.equivReal. Transcendentals (exp, log, etc.) are already transported in LogicRealTranscendentals; this module is the constant layer on that same carrier.

RS-native units set $c=1$, with $\hbar=\varphi^{-5}$ and $G=\varphi^5/\pi$. The golden ratio $\varphi$ is the self-similar fixed point forced at T6; the eight-tick octave (period $2^3$) is T7. The EM certificate records $\alpha^{-1}=\alpha_{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$ with $\alpha_{\mathrm{seed}}=4\pi$ and $f_{\mathrm{gap}}=w_8\ln\varphi$, landing in $(137.030,137.039)$.

Named exports include $\varphi_L$, tick, octave, J-bit, coherence energy, $\hbar_L$, gravity, Einstein $\kappa$, and $\alpha^{-1}_L$, plus toReal_* bridges for the first few.

proof idea

Definition-and-transport module, not a theorem development. Each constant is introduced as a LogicReal value (typically by pulling the ordinary RS constant across the equivalence, or by composing already-transported transcendentals). Companion lemmas of the form toReal_phiL, toReal_tickL, toReal_octaveL are one-line transport identities: applying LogicReal.toReal recovers the Mathlib real constant already fixed in Constants / Constants.Alpha / EMAlphaCert. No independent analytic argument lives here.

why it matters in Recognition Science

Gives every later LogicReal-native development a single import for RS units instead of ad-hoc transports. Immediate consumer is Cost.JcostLogic, the reciprocal cost $J$ on recovered reals: that module mirrors Cost.JcostCore and reduces theorems through LogicReal.toReal, so it needs $\varphi_L$ and related yardsticks on the same carrier.

Anchors the forcing-chain landmarks T6 ($\varphi$) and T7 (eight-tick octave) inside the recovered line, and exposes the certified $\alpha^{-1}$ band for EM work without leaving LogicReal. Without this layer, cost and coupling proofs would repeatedly re-derive transport of constants.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (25)