pith. sign in
module module high

IndisputableMonolith.Foundation.ConstantDerivations

show as:
view Lean formalization →

This module derives the core physical constants of Recognition Science in native units from the upstream forcing results. It defines J_bit as ln(phi) along with c_rs = 1, G_rs = phi^5/pi, and their positivity and algebraic properties. Researchers completing the forcing chain to observable physics would cite these equalities. The module consists of targeted definitions and direct equalities with no separate proofs.

claim$J_{ m bit} = m ln(\phi)$, $c_{ m rs} = 1$, $G_{ m rs} = rac{ m phi^5}{ m pi}$, with $J_{ m bit} > 0$, $c_{ m rs} > 0$, $G_{ m rs} > 0$, and the algebraic relations among them.

background

The module imports PhiForcing (phi forced by self-similarity in a discrete ledger with J-cost), DimensionForcing (D = 3 forced), and LawOfExistence (x exists iff defect(x) = 0). It builds directly on the J-cost structure and the phi-ladder to express constants in RS units where c = 1 by construction. The supplied doc-comment identifies the fundamental bit cost as J_bit = ln(phi).

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the constant derivations required by the master forcing-chain theorem in RealityFromDistinction, which starts from a single distinction and reaches spacetime, the light cone, and the phi-derived constants. It closes the step from abstract forcing (T5-T8) to explicit values for c, G, and the bit cost.

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)