pith. machine review for the scientific record. sign in
def definition def or abbrev high

synapse_cost

show as:
view Lean formalization →

The synapse cost is defined as the J-cost of the ratio between two firing rates. Researchers modeling local cache benefits or Hebbian covariance in Recognition Science cite this definition. It is a direct one-line wrapper that applies the established J-cost function to the firing-rate ratio.

claimFor firing rates $f_u$ and $f_v$, the synapse cost equals $J(f_u/f_v)$, where $J(x)=(x+x^{-1})/2-1$ is the J-cost function.

background

The Local Cache Theorem module establishes that caching reduces total access cost under assumptions A1-A3, with the J-cost function serving as the primitive cost measure. J-cost is the cost of a recognition event, derived from multiplicative recognizers as the comparator cost on positive ratios, and satisfies non-negativity with a minimum at argument 1. Upstream results from observer forcing and multiplicative recognizer L4 confirm that J-cost obeys the Recognition Composition Law and is strictly increasing on (1, ∞) with symmetry under inversion.

proof idea

The definition is a one-line wrapper that applies the J-cost function directly to the ratio of the two firing rates.

why it matters in Recognition Science

This definition supports the local cache benefit and Hebbian sign structure results in the module by quantifying synaptic cost. It realizes the mathematical content of Hebb's rule that correlated firing (ratio near 1) minimizes cost. It connects to the Recognition Composition Law and the phi-ladder in the forcing chain from T5 onward.

scope and limits

formal statement (Lean)

 183noncomputable def synapse_cost (f_u f_v : ℝ) : ℝ :=

proof body

Definition body.

 184  Jcost (f_u / f_v)
 185
 186/-- **KEY LEMMA**: J-cost is strictly increasing on (1, ∞).
 187    For r > 1, J(r) > J(1) = 0. Combined with J(r) = J(1/r),
 188    this means any deviation from r = 1 increases cost.
 189
 190    This is the mathematical content of Hebb's rule: correlated firing (r ≈ 1)
 191    has minimal cost; uncorrelated firing (r ≠ 1) has positive cost. -/

depends on (13)

Lean names referenced from this declaration's body.