toReal_EcohL
plain-language theorem explainer
Transporting the LogicReal coherence scale back along the recovered-real equivalence yields the Mathlib constant E_coh. Anyone equating RS constants on the logic-derived line with the existing Constants bundle cites this identity. The proof is a one-line application of the round-trip lemma toReal_fromReal.
Claim. If $E_{\mathrm{coh}}^{L}$ denotes the coherence scale lifted into the recovered real line via $\mathrm{fromReal}$, then $\mathrm{toReal}(E_{\mathrm{coh}}^{L}) = E_{\mathrm{coh}}$, where $E_{\mathrm{coh}}$ is the Mathlib real coherence energy from the RS constants bundle.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line (LogicReal). Each constant is defined by lifting a Mathlib real through fromReal; companion simp lemmas show that toReal undoes the lift and recovers the original value.
EcohL is the recovered coherence scale: EcohL := fromReal Constants.E_coh. The map toReal : LogicReal → ℝ is CompareReals.compareEquiv on the underlying value; fromReal is the inverse embedding. The upstream round-trip theorem states toReal (fromReal x) = x for every Mathlib real x.
Constants.E_coh is the coherence-energy yardstick used elsewhere in the monolith (mass ladder, CPM existence law). This module only certifies that the LogicReal copy is faithful under transport, not that the numerical value is forced from first principles.
proof idea
One-line wrapper. Unfold EcohL to fromReal Constants.E_coh and apply the general round-trip lemma toReal_fromReal, which simplifies toReal (fromReal x) = x by unfolding toReal and fromReal and using the comparison equivalence.
why it matters
Closes the transport identity for the coherence scale inside the LogicReal constants suite (siblings: phiL, tickL, hbarL, gravL, alphaInvL and their toReal lemmas). Downstream code that rewrites goals involving toReal EcohL can discharge them by simp without re-proving the round trip.
In the broader RS picture the coherence energy is the yardstick in the mass formula (yardstick · φ^(rung−8+gap(Z))). Faithful LogicReal mirroring keeps foundation-level arguments about that yardstick aligned with the Mathlib Constants API. No used_by edges are recorded yet; the lemma is infrastructure for later foundation and verification modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.