Pith. sign in
module module high

IndisputableMonolith.Compat.Constants

show as:
view Lean formalization →

Compat.Constants supplies compatibility definitions for core Recognition Science values including the golden ratio phi and a placeholder cohesion energy E_coh. It re-exports shims from the main Constants module for use in cross-module compatibility layers. The module contains only definitions and positivity statements.

claim$\phi$ is the golden ratio, $E_{\rm coh}$ is the cohesion energy placeholder, $\tau_0 = 1$ tick is the fundamental RS time quantum, and $l_0$, rung are the associated length and rung parameters.

background

The module imports IndisputableMonolith.Constants, whose doc states: 'The fundamental RS time quantum (RS-native). $\tau_0 = 1$ tick.' It introduces sibling definitions phi, E_coh, tau0, l0, rung together with their positivity lemmas. The Compat domain provides shims so that downstream code can reference these constants without direct dependence on the core file.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds IndisputableMonolith.Compat, described as 'Central compatibility imports for the project. Downstream modules can import this file to gain access to compatibility shims and project-wide constants.' It supplies the placeholder cohesion energy and related constants required by the compatibility layer.

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)