JbitL
plain-language theorem explainer
Defines the J-bit constant on the recovered real line as the natural logarithm of the recovered golden ratio. Anyone working with RS elementary cost units inside LogicReal cites this. The body is a one-line composition of the transported log with the recovered phi.
Claim. On the recovered real line, the J-bit constant is $\log_L(\varphi_L)$, where $\varphi_L$ is the recovered golden ratio and $\log_L$ is the natural logarithm transported from $\mathbb{R}$.
background
LogicRealConstants mirrors Recognition Science constants on LogicReal, the Cauchy completion of the recovered rationals (via Bourbaki completion of $\mathbb{Q}$ and the LogicRat equivalence). Each constant is written in LogicReal; companion theorems show that toReal recovers the ordinary real constant from IndisputableMonolith.Constants.
The golden ratio on this line is $\varphi_L = (1 + \sqrt{5}_L)/2$. The natural log logL is the transport fromReal (Real.log (toReal x)). In RS the elementary J-bit is $\ln\varphi$, the log-scale set by the self-similar fixed point forced at T6; this definition places that unit on LogicReal.
proof idea
Pure definition: assign JbitL to the application of the transported natural logarithm logL to the recovered golden ratio phiL. No proof obligations.
why it matters
Supplies the LogicReal carrier for the RS J-bit so downstream transport can match the classical constant. The immediate consumer is toReal_JbitL, which simp-reduces toReal JbitL = Constants.J_bit via the definitions of JbitL and Constants.J_bit.
In the forcing chain, T5 fixes the J-cost $J(x)=(x+x^{-1})/2-1$ and T6 forces $\varphi$ as the self-similar fixed point; the bit scale $\ln\varphi$ is the natural log-unit tied to that fixed point. Placing it on LogicReal keeps the constant layer aligned with the recovered-real development rather than only on Mathlib $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.