SalienceLean

Proposition 2 (translation invariance). Adding a constant to every score leaves all selection probabilities unchanged, for every temperature.

Proposition 3 (low-temperature limit). As T → 0⁺ the probability of the unique maximizer tends to 1; tendsto_softmax_nhdsGT_zero_of_lt sends any strictly dominated candidate to 0.

Proposition 3 (high-temperature limit). As T → ∞ every selection probability tends to the uniform value 1/|I|.

Proposition 4 (conservation and sparsity). Allocated budgets sum to B, and candidates with non-positive score receive zero. In addition, 0 ≤ bᵢ ≤ B.

Veto gate. If the continuity factor is zero, the score is zero, independently of the value terms.

Time decay. Under positive value terms, gates, and decay rate, the score is strictly decreasing in the age Δt.

Potential form (eqs. 9–10). For positive gate factors and normalizer, the score equals ρ · e^(−Φ), with Φ the salience potential.

Rescaling all scores and the temperature by a common nonzero factor leaves the policy unchanged; only the ratio S/T is observable.

Non-identifiability. The regime logit log S + βχ is invariant under S ↦ S·e^h, χ ↦ χ − h/β; at a single stake β, prior salience and evidence are not separately identifiable.

theorem logit_gauge {β : ℝ} (hβ : β ≠ 0) {S : ℝ} (hS : 0 < S) (χ h : ℝ) :
    log (S * exp h) + β * (χ - h / β) = log S + β * χ

Identification at two stakes. Logits observed at two values of β determine the evidence term and the log prior.

Rows of the Fisher matrix diag(p) − ppᵀ sum to zero: the all-ones direction of logit space is null, the same gauge in infinitesimal form.

Optimality. Every distribution satisfies ⟪p,ℓ⟫ + T·H(p) ≤ T log Z, and the softmax policy attains the bound.

Uniqueness. Equality holds only at the softmax policy, via a strict Gibbs inequality (sum_mul_log_sub_log_neg).

theorem objective_eq_free_energy_iff [Nonempty ι] {T : ℝ} (hT : 0 < T) (ℓ : ι → ℝ)
    {p : ι → ℝ} (hp : ∀ i, 0 ≤ p i) (hps : ∑ i, p i = 1) :
    (∑ i, p i * ℓ i) + T * (-∑ i, p i * log (p i)) = T * log (∑ j, exp (ℓ j / T))
      ↔ p = softmax T ℓ

Perturbation bound. If the leading score exceeds every other by more than 2ε, no ε-perturbation of the scores changes the argmax.

For square invertible C, a charge conserved by F and transported contragrediently (q_c ᵥ* C = q_f) is conserved by C Fᵐ C⁻¹ — a change of coordinates with temporal blocking.

Lossy case. For rectangular C with C F = Fc C, the transported charge is conserved along every coarse trajectory arising from a fine state; no invertibility or rank hypothesis.

theorem coarse_charge_conserved_of_intertwines {C : Matrix m n ℝ} {F : Matrix n n ℝ}
    {Fc : Matrix m m ℝ} {qf : n → ℝ} {qc : m → ℝ}
    (hinter : C * F = Fc * C) (hf : qf ᵥ* F = qf) (htrans : qc ᵥ* C = qf) (x : n → ℝ) :
    qc ⬝ᵥ (Fc *ᵥ (C *ᵥ x)) = qc ⬝ᵥ (C *ᵥ x)

A charge of the form q = q_c ᵥ* C is computable from Cx alone, and vanishes on ker C. Sufficiency and its corollary; the converse is not formalized (see Scope).

The antisymmetric mode of a symmetric two-state leakage channel is an eigenvector with eigenvalue 1 − 2ε; the charge scales as (1−2ε)^t and tends to 0 for 0 < ε < 1.

Majority decoding over three copies gives the map ε ↦ 3ε² − 2ε³: contraction below ε = 1/2, growth above it, and derivative 3/2 at the fixed point, so the threshold repels.