toReal_JbitL
plain-language theorem explainer
Transport of the recovered J-bit on the logic-real line equals the classical real constant J_bit. Anyone bridging LogicReal constants to IndisputableMonolith.Constants cites this simp lemma. The proof is a one-line simp that unfolds both sides to the same real logarithm of φ.
Claim. If $J^{\mathrm{bit}}_L$ denotes the recovered J-bit on the logic-real line (defined as $\log_L \varphi_L$), then its transport $\mathrm{toReal}(J^{\mathrm{bit}}_L)$ equals the classical real constant $J_{\mathrm{bit}}$.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line LogicReal. Each constant is defined in that type; companion theorems show that toReal (the comparison equivalence into Mathlib's ℝ) recovers the matching entry of IndisputableMonolith.Constants.
The recovered J-bit is JbitL := logL phiL: the logic-real logarithm of the recovered golden ratio. Upstream, toReal on LogicReal is the transport map CompareReals.compareEquiv applied to the underlying value; sibling lemmas already identify toReal phiL with the classical φ. The classical target Constants.J_bit is the real-side J-bit (definitionally the real log of φ once unfolded).
Local setting: a thin bridge layer so later development can stay in LogicReal and discharge equalities into Mathlib reals by simp.
proof idea
One-line simp wrapper. Unfolding JbitL (to logL phiL) and Constants.J_bit reduces both sides to the same real expression, so simp closes the goal with no further lemmas.
why it matters
Closes the J-bit slot in the LogicReal-to-Constants dictionary, parallel to the sibling transports for φ, the tick, and the octave. Downstream use is not yet wired in this graph, but the lemma is the natural simp fact whenever a proof must move a J-bit identity from the recovered line onto Mathlib ℝ.
In the framework, the J-cost is the unique cost forced by the Recognition Composition Law (T5), and φ is the self-similar fixed point (T6). Identifying the recovered J-bit with log φ keeps that cost unit aligned across the two real presentations. No open scaffold is involved: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.