Module aggressiveness 

Single 0.0–1.0 compression-intensity knob.

TTC-style UX parity: callers (the ctx_read tool, the proxy, the CLI) can express “how hard should I compress?” as one number instead of picking among the ten read modes. The number is mapped onto the existing density / entropy / information-bottleneck stages — it never introduces a model, so the #498 determinism contract (output = pure function of inputs) is preserved.

Resolution order (see effective): explicit per-call arg > the LEAN_CTX_AGGRESSIVENESS env var > [compression] compression_aggressiveness in config > None. None means “use each mode’s current default”, i.e. the behaviour shipped before this knob existed.

Structs

AggressivenessProfile

Concrete tuning derived from one aggressiveness value. Every field is a pure function of a, so the same a always yields the same knobs (determinism).

Functions

cache_fragment

Stable cache-key fragment for an aggressiveness setting.

effective

Resolves the effective aggressiveness from (in priority order) an explicit per-call value, the LEAN_CTX_AGGRESSIVENESS env var, and the config field. Returns None when nothing is set so callers keep their current defaults.