pith. sign in
module module high

IndisputableMonolith.Common.CanonicalJBand

show as:
view Lean formalization →

The module defines the canonical recognition cost J(x) = ½(x + 1/x) - 1 together with its immediate variants. Acoustics, astrophysics, and chemistry modules cite it to locate thresholds at the J(φ) band. It consists entirely of definitions with no proofs or derivations.

claimThe canonical recognition cost is $J(x) = ½(x + x^{-1}) - 1$.

background

This module supplies the core J function used throughout the Recognition Science framework. J measures recognition cost in RS-native units where the base time quantum τ₀ equals one tick. The definition matches the closed-form expression J(x) = cosh(log x) - 1 and is accompanied by elementary variants such as J_one, J_reciprocal, J_phi_pos, and J_phi_band.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the J-cost definition to forty downstream modules. These apply the canonical J(φ) band to ultrasound therapy thresholds, stellar evolution phases, accretion-disk transitions, magnetic reconnection rates, and enzyme catalysis mechanisms. The module therefore anchors the common layer that feeds every J-cost application.

scope and limits

used by (40)

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

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)