Pith. sign in
module module high

IndisputableMonolith.Common.CanonicalJBand

show as:
view Lean formalization →

The CanonicalJBand module defines the canonical recognition cost J(x) = ½(x + 1/x) - 1 together with band and certification helpers. Researchers modeling thresholds in ultrasound therapy, stellar evolution, accretion disks, magnetic reconnection, and enzyme catalysis cite these definitions to locate RS-native transition points. The module consists entirely of definitions with no proofs.

claim$J(x) = \frac12\left(x + \frac1x\right) - 1$

background

Recognition Science measures recognition effort via the J-cost on positive ratios. The module CanonicalJBand sits in the Common layer and supplies the explicit functional form of J along with its values at the self-similar fixed point phi. It imports the RS time quantum τ₀ = 1 tick from Constants.

The supplied definition matches the T5 J-uniqueness landmark: J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1. Sibling definitions include J_one, J_reciprocal, J_phi_pos, J_phi_band, J_inv_phi_sq_pos and the certification predicate CanonicalCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the J function required by forty downstream modules, including UltrasoundTherapyFromJCost, StellarEvolutionFromJCost, AccretionDiskFromJCost, MagneticReconnectionFromJCost and CatalysisFromJCost. It implements the J-uniqueness step of the T0-T8 forcing chain, enabling all later claims that physical thresholds occur inside the canonical J(φ) band.

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)