Yang's Tolerance Principle [Yan16]

A productivity criterion for rule learning. Given a rule with n items in its scope and e exceptions (items in scope that fail to obey the rule), the rule is tolerated (treated as productive) iff

e ≤ n / ln n.

Below this threshold, the cost of memorizing exceptions is outweighed by the generality of the rule; above it, the learner abandons the rule and treats the items as lexically listed. The threshold θ_N = N / ln N is derived in [Yan16] from a sufficiency condition for the Elsewhere Condition under serial rule access.

This module defines the threshold and the productivity predicate. It is deliberately minimal — actual numerical certificates for specific (n, e) pairs are deferred to the study files that need them.

[Bel26] invokes the principle as the productivity gate inside the D2L tier-learner; see Studies/Belth2026.lean. Other potential consumers (Yang's morphological productivity, infant rule generalization [emond-shi-2021]) are not yet wired in.

noncomputable def Yang2016.threshold (n : ℕ) : ℝ

The tolerance threshold for a vocabulary of size n. When n ≤ 1, Real.log n ≤ 0 and the threshold collapses (mathlib's convention makes division by zero return zero) — productivity in the trivial case is governed by tolerates's pointwise definition, not by interpreting the threshold as a positive bound.

Equations

• Yang2016.threshold n = ↑n / Real.log ↑n

def Yang2016.tolerates (n e : ℕ) : Prop

A rule with n items in scope and e exceptions is tolerated iff the exception count fits under Yang's threshold.

Equations

• Yang2016.tolerates n e = (↑e ≤ Yang2016.threshold n)

theorem Yang2016.threshold_nonneg (n : ℕ) : 0 ≤ threshold n

The threshold is nonnegative for every n. For n ≥ 1, both numerator and denominator are nonnegative; for n = 0, mathlib's Real.log 0 = 0 makes the quotient 0 / 0 = 0.

theorem Yang2016.tolerates_zero (n : ℕ) : tolerates n 0

A rule with no exceptions is always tolerated.