Pith. sign in
module module high

IndisputableMonolith.Foundation.ConstantDerivations

show as:
view Lean formalization →

The ConstantDerivations module supplies explicit RS-native expressions for the bit cost and derived constants. Researchers tracing the forcing chain from self-similarity to measurable quantities would cite it when converting J-cost into c, G, and the alpha band. The module consists of targeted definitions together with short positivity and equality proofs that rest directly on the imported PhiForcing, DimensionForcing, and LawOfExistence results.

claim$J_{ m bit}=\ln\phi$, $E_{ m coh}$ the coherent energy scale, period 8 the eight-tick octave, $c=1$, $\hbar=\phi^{-5}$, $G=\phi^5/\pi$, and $\alpha^{-1}\in(137.030,137.039)$.

background

The module follows the three upstream modules whose doc-comments define the setting. PhiForcing shows that self-similarity on a discrete ledger with J-cost forces the golden ratio. DimensionForcing establishes that spatial dimension D=3 is forced. LawOfExistence equates existence to zero defect. ConstantDerivations then converts these structures into concrete constants by setting the fundamental bit cost J_bit = ln(φ) and building the remaining quantities from it.

proof idea

This is a definition module whose content is a sequence of abbrevs and short theorems. Each constant (J_bit, E_coh, c_rs, G_rs, period_8) receives an explicit algebraic definition in terms of φ; the accompanying _pos and _eq lemmas are one-line wrappers that apply the positivity and equality results already proved in PhiForcing and DimensionForcing.

why it matters in Recognition Science

The derivations supply the concrete constants required by the master forcing-chain theorem in RealityFromDistinction, which starts from a single distinction and reaches spacetime together with the physical constants. The module therefore closes the step that converts the abstract J-cost and phi-ladder into the RS-native values c=1, G=φ^5/π, and the alpha interval cited in the framework landmarks.

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)