pith. sign in
module module high

IndisputableMonolith.Compat.Constants

show as:
view Lean formalization →

Compat.Constants supplies RS-native constants including the golden ratio phi and a placeholder cohesion energy E_coh. It also defines tau0 as the fundamental time quantum equal to one tick along with l0 and rung. Researchers building models in the Recognition framework import this module for compatibility shims. The module is a thin import layer over the core Constants module with no internal proofs.

claimThe module provides definitions for the golden ratio $phi > 0$, cohesion energy placeholder $E_{coh}$, fundamental time quantum $tau_0 = 1$ tick, length scale $l_0$, and rung index, together with their positivity statements.

background

This module belongs to the Compat domain and imports IndisputableMonolith.Constants, whose doc states that the fundamental RS time quantum (RS-native) is tau0 equal to 1 tick. It introduces sibling definitions phi, phi_pos, E_coh, E_coh_pos, tau0, tau0_pos, l0, l0_pos, and rung. These supply the basic scales and the phi-ladder used throughout RS-native units where c equals 1.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds the central compatibility imports for the project in IndisputableMonolith.Compat. Downstream modules import this file to gain access to compatibility shims and project-wide constants. It supports the framework by exposing placeholder constants such as cohesion energy for later refinement.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)