Pith. sign in
module module high

IndisputableMonolith.Foundation.LogicRealConstants

show as:
view Lean formalization →

Defines Recognition Science fundamental constants on the recovered LogicReal line: golden ratio, tick, eight-tick octave, J-bit, coherence energy, ħ, G, Einstein κ, and α⁻¹. Transport lemmas identify each with its Mathlib real counterpart via the LogicReal equivalence. Downstream LogicReal cost and physics layers import this as the native constant surface. Structure is definitional bindings plus toReal equalities, not a deep derivation.

claimOn the recovered real line $\mathrm{LogicReal}$, the module introduces $\varphi_L$, the tick $\tau_L$, the octave period $2^3$, $J_{\mathrm{bit},L}$, $E_{\mathrm{coh},L}$, $\hbar_L$, $G_L$, $\kappa_{E,L}$, and $\alpha^{-1}_L$, with transport equalities $\mathrm{toReal}(c_L)=c$ matching each Mathlib $\mathbb{R}$ RS constant (including the certified $\alpha^{-1}$ band).

background

Recognition Science works in RS-native units with $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, and $\alpha^{-1}$ forced into $(137.030,137.039)$. The golden ratio $\varphi$ is the self-similar fixed point (forcing step T6); the eight-tick octave is period $2^3$ (T7). The ordinary Mathlib constants live in Constants and Constants.Alpha; the EM certificate records the assembled coupling $\alpha^{-1}=\alpha_{\mathrm{seed}}\cdot\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$ with $\alpha_{\mathrm{seed}}=4\pi$ and $f_{\mathrm{gap}}=w_8\ln\varphi$, not a fit to the infrared measurement.

LogicReal is the recovered real line, equivalent to Mathlib $\mathbb{R}$ by LogicReal.equivReal. LogicRealTranscendentals transports standard transcendental functions across that equivalence so later modules can stay on LogicReal and reduce proofs by toReal. This module is the constant layer of that transport: each RS landmark is named as a LogicReal value and tied back to the already-verified real constant.

proof idea

Definition module, not a theorem development. Each constant (phiL, tickL, octaveL, JbitL, EcohL, hbarL, gravL, kappaEinsteinL, alphaInvL) is introduced by transport or direct binding from the Mathlib/RS constant surface. Companion lemmas (toReal_phiL, toReal_tickL, toReal_octaveL, and siblings) are one-line transport equalities through LogicReal.toReal / the real equivalence. No independent forcing or numerical derivation happens here; those live upstream in Constants, Alpha, and EMAlphaCert.

why it matters in Recognition Science

Gives the LogicReal physics stack a single native constant dictionary so cost and dynamics never drop to bare Mathlib reals mid-argument. Immediate consumer is Cost.JcostLogic, the reciprocal cost on recovered reals: a transport mirror of Cost.JcostCore whose definitions live on LogicReal and whose proofs reduce through toReal. That cost is the J-functional side of the Recognition Composition Law and the T5 uniqueness story ($J(x)=(x+x^{-1})/2-1$). By pinning $\varphi$, the tick/octave, $\hbar$, $G$, and the certified $\alpha^{-1}$ band on LogicReal, the module keeps the forcing-chain landmarks (T6 $\varphi$, T7 eight-tick) available wherever LogicReal reasoning continues.

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)