pith. sign in
module module high

IndisputableMonolith.Foundation.ConstantDerivations

show as:
view Lean formalization →

This module assembles the RS-native expressions for fundamental constants once phi and D=3 are forced. Researchers tracing the forcing chain cite it for the bit cost and unit choices that close the constants layer. Content consists of targeted definitions and direct equalities that rest on the imported PhiForcing and DimensionForcing results.

claim$J_{ m bit}=\ln\phi$, $c_{ m rs}=1$, $G_{ m rs}=\phi^5/\pi$, together with the eight-tick period and positivity statements for the derived quantities.

background

The module belongs to the Foundation layer and imports PhiForcing (phi forced by self-similarity on a discrete ledger carrying J-cost), DimensionForcing (D=3 forced by four independent arguments), and LawOfExistence (x exists iff defect(x)=0). J-cost is the functional J(x)=(x+x^{-1})/2-1. The local theoretical setting is the extraction of concrete constants after the T5-T8 steps of the unified forcing chain have fixed phi and spatial dimension.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The derivations supply the explicit algebraic forms for c, G, and the bit cost that are required by the master forcing-chain theorem in RealityFromDistinction, which starts from a single distinction and reaches spacetime together with the phi-derived constants.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (20)