E_coh
plain-language theorem explainer
E_coh supplies the cohesion energy as a real number drawn from the abstract Constants bundle in the LawOfExistence module. Researchers modeling energy scales on the phi-ladder in Recognition Science reference this placeholder for cohesion calculations. The definition is a direct one-line alias with no reduction or additional lemmas.
Claim. The cohesion energy $E_{coh} : ℝ$ is the placeholder value taken from the CPM constants structure whose fields include nonnegative $K_{net}$, $C_{proj}$, $C_{eng}$ and $C_{disp}$.
background
The Compat.Constants module collects project-wide constants and minimal structural lemmas for the Recognition Science framework. The upstream Constants structure from CPM.LawOfExistence bundles the core parameters with the explicit nonnegativity condition on Knet. Cohesion energy serves as a placeholder for energy computations linked to the J-cost function and the self-similar fixed point phi.
proof idea
The declaration is a one-line wrapper that aliases E_coh directly to the corresponding definition in IndisputableMonolith.Constants, which draws from the upstream Constants structure.
why it matters
This definition supplies the cohesion energy placeholder required for energy-scale work in the Recognition framework. It supports mass formulas of the form yardstick times phi to a power and relates to the Berry creation threshold. With zero downstream uses recorded, its precise placement relative to the T5-T8 forcing chain and the eight-tick octave remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.