Pith. sign in
module module high

IndisputableMonolith.Foundation.LogicRealTranscendentals

show as:
view Lean formalization →

Module supplying definitions for square root, exponential, logarithm, power, pi, sine, cosine, sinh and cosh on reals recovered from the logic rationals. Researchers needing analytic operations on LogicReal would cite these transports. The module consists entirely of definition wrappers transporting Mathlib functions.

claimDefinitions of $\sqrt_L$, $\exp_L$, $\log_L$, $\mathrm{rpow}_L$, $\pi_L$, $\sin_L$, $\cos_L$, $\sinh_L$, $\cosh_L$ (and their $\mathrm{toReal}$ variants) on the recovered reals $\mathbb{R}_L$ obtained from LogicRat via Bourbaki completion.

background

RealsFromLogic recovers the real numbers from the Law-of-Logic rational layer. Its doc states: 'Recovery of the real numbers from the Law-of-Logic rational layer. The construction uses Mathlib's Bourbaki completion of ℚ as the completion engine, while the input rationals are the recovered rationals LogicRat from Foundation.RationalsFromLogic.' This module extends that recovered real type by transporting the standard transcendental functions from Mathlib.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the transcendental functions required to define physical constants and operations on the recovered reals, extending the real recovery in RealsFromLogic to support later constructions such as the phi-ladder and mass formulas in the Recognition framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (23)