IndisputableMonolith.Foundation.LogicRealTranscendentals
This module supplies logic-native versions of square root, exponential, logarithm, pi, sine, cosine, sinh and cosh on the reals recovered from the Law-of-Logic rationals. Researchers extending the Recognition Science foundation to analytic operations inside the logic-derived number system would cite these definitions. The module consists entirely of transport definitions that embed the corresponding Mathlib operations through the RealsFromLogic recovery map.
claimThe module defines transported functions such as $sqrt_L : R_L to R_L$, $exp_L : R_L to R_L$, $log_L : R_L to R_L$, $pi_L : R_L$, $sin_L : R_L to R_L$, $cos_L : R_L to R_L$, $sinh_L : R_L to R_L$ and $cosh_L : R_L to R_L$, where $R_L$ denotes the reals obtained by Bourbaki completion of the logic rationals $LogicRat$, each obtained by transport from the corresponding $Real$ operation.
background
The module builds directly on the recovery of real numbers from the Law-of-Logic rational layer. RealsFromLogic.lean constructs these reals via Mathlib's Bourbaki completion of the rationals, taking as input the recovered rationals LogicRat from Foundation.RationalsFromLogic. In other words, the reals arise as the metric completion of the logic-derived rationals under the standard absolute value. The present module then equips these recovered reals with the standard transcendental operations by transporting the Mathlib implementations.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the analytic operations required for later stages of the Recognition Science derivation, including the definition of constants such as pi and the hyperbolic functions that appear in the J-uniqueness relation and the phi-ladder mass formulas. It feeds the eight-tick octave and spatial-dimension forcing steps by making real analysis available inside the logic foundation, even though the current dependency graph lists no immediate downstream declarations.
scope and limits
- Does not prove any identities or continuity statements for the transported functions.
- Does not construct the reals from first principles but relies on the upstream RealsFromLogic embedding.
- Does not introduce new axioms or extend the logic rationals.
- Does not define arithmetic operations, which remain in the RealsFromLogic module.
depends on (1)
declarations in this module (23)
-
def
sqrtL -
def
expL -
def
logL -
def
rpowL -
def
piL -
def
sinL -
def
cosL -
def
sinhL -
def
coshL -
theorem
toReal_sqrtL -
theorem
toReal_expL -
theorem
toReal_logL -
theorem
toReal_rpowL -
theorem
toReal_piL -
theorem
toReal_sinL -
theorem
toReal_cosL -
theorem
toReal_sinhL -
theorem
toReal_coshL -
theorem
expL_pos -
theorem
sqrtL_nonneg -
theorem
expL_logL -
theorem
logL_expL -
theorem
coshL_eq_exp