Certified atoms for transcendental RSA models

RSA models with real-exponent utilities or exponential costs reduce, after exact-rational bookkeeping, to a handful of named transcendental atoms: n-th roots of explicit rationals (softmax utilities with denominator-n weights) and exp of negated rational costs. This file provides the atoms and their two-sided rational-bound certificates, so study-level predictions close by nlinarith over kernel-checked power inequalities.

• rootAtom X n is X ^ (n⁻¹ : ℝ): bound it by exhibiting r ^ n ≤ X and X ≤ s ^ n, both kernel-checkable when r, s, X are rational.
• expAtom q is exp (−q): for rational q = m / n the identity expAtom q ^ n * exp m = 1 turns digit bounds on e into two-sided bounds on the atom.

Main results

• le_rootAtom_of_pow_le, rootAtom_le_of_le_pow, rootAtom_mem_Icc — n-th-root certificates.
• rootAtom_eq_exp — the bridge to the paper-facing exp/log form.
• expAtom_pow_mul_exp_eq_one — the inversion identity for cost atoms.

Root atoms

noncomputable def RSA.rootAtom (X : ℝ) (n : ℕ) : ℝ

The n-th root of X as a real power. For rational X this is the shape of softmax utilities with denominator-n weights.

Equations

• RSA.rootAtom X n = X ^ (↑n)⁻¹

theorem RSA.rootAtom_pos {X : ℝ} (hX : 0 < X) (n : ℕ) : 0 < rootAtom X n

theorem RSA.le_rootAtom_of_pow_le {r X : ℝ} {n : ℕ} (hn : n ≠ 0) (hr : 0 ≤ r) (h : r ^ n ≤ X) : r ≤ rootAtom X n

Lower certificate: r ^ n ≤ X gives r ≤ ⁿ√X (mathlib's Real.le_rpow_inv_iff_of_pos at a natural exponent).

theorem RSA.rootAtom_le_of_le_pow {X s : ℝ} {n : ℕ} (hn : n ≠ 0) (hX : 0 ≤ X) (hs : 0 ≤ s) (h : X ≤ s ^ n) : rootAtom X n ≤ s

Upper certificate: X ≤ s ^ n gives ⁿ√X ≤ s (mathlib's Real.rpow_inv_le_iff_of_pos at a natural exponent).

theorem RSA.rootAtom_mem_Icc {r X s : ℝ} {n : ℕ} (hn : n ≠ 0) (hr : 0 ≤ r) (hX : 0 ≤ X) (hs : 0 ≤ s) (hlo : r ^ n ≤ X) (hhi : X ≤ s ^ n) : rootAtom X n ∈ Set.Icc r s

Two-sided certificate from kernel-checkable power bounds.

theorem RSA.rootAtom_eq_exp {X : ℝ} (hX : 0 < X) (n : ℕ) : rootAtom X n = Real.exp (Real.log X / ↑n)

Bridge to the paper-facing exponential form: ⁿ√X = exp (log X / n) for positive X. (The log X * n⁻¹ orientation is what rpow_def_of_pos produces; commute afterwards as needed.)

theorem RSA.rootAtom_pow_mul_pow {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (j k n : ℕ) : rootAtom (a ^ j * b ^ k) n = Real.exp (↑j / ↑n * Real.log a + ↑k / ↑n * Real.log b)

The two-factor exponential form: the n-th root of a^j · b^k is the weighted geometric mean exp ((j/n)·log a + (k/n)·log b) — the shape of softmax utilities with denominator-n noise weights.

Two-factor geometric means

b ^ w * a ^ (1 − w) is the channel-weighted geometric mean of two literal posteriors — eq.-7-style speaker utilities for a binary-support noise channel. The strict bounds against a comparison value need no magnitude computation: a weighted GM sits strictly between its factors.

theorem RSA.rpow_mul_rpow_lt {a b c w w' : ℝ} (ha : 0 < a) (hc : 0 < c) (hb : 0 < b) (hbc : b ≤ c) (hac : a < c) (hw : 0 ≤ w) (hw' : 0 < w') (hsum : w + w' = 1) : b ^ w * a ^ w' < c

A two-factor GM is strictly below c when one factor is at most c and the other strictly below, its weight positive.

theorem RSA.lt_rpow_mul_rpow {a b c w w' : ℝ} (hc : 0 < c) (ha : c < a) (hcb : c ≤ b) (hw : 0 ≤ w) (hw' : 0 < w') (hsum : w + w' = 1) : c < b ^ w * a ^ w'

A two-factor GM is strictly above c when one factor is at least c and the other strictly above, its weight positive.

Exponential cost atoms

noncomputable def RSA.expAtom (q : ℝ) : ℝ

The multiplicative cost factor exp (−q) for a cost q.

Equations

• RSA.expAtom q = Real.exp (-q)

theorem RSA.expAtom_pos (q : ℝ) : 0 < expAtom q

theorem RSA.expAtom_pow_mul_exp_eq_one {m : ℝ} {n : ℕ} (hn : n ≠ 0) : expAtom (m / ↑n) ^ n * Real.exp m = 1

The inversion identity: for q = m / n, expAtom q ^ n · exp m = 1. Combined with digit bounds on exp m (from Real.exp_one_gt_d9 / exp_one_lt_d9 raised by pow_lt_pow_left₀), this yields two-sided rational bounds on the atom via kernel-checked power comparisons.

theorem RSA.expAtom_pow_mul_exp_nat_mul {q : ℝ} (n : ℕ) : expAtom q ^ n * Real.exp (↑n * q) = 1

Power form of the inversion identity, stated at the atom's own exponent (no division shape): expAtom q ^ n · exp (n·q) = 1.

theorem RSA.lt_expAtom {q r : ℝ} {n : ℕ} (hn : n ≠ 0) (hr : 0 ≤ r) (h : r ^ n * Real.exp (↑n * q) < 1) : r < expAtom q

Lower certificate: r ^ n · exp (n·q) < 1 gives r < expAtom q.

theorem RSA.expAtom_lt {q s : ℝ} {n : ℕ} (hn : n ≠ 0) (hs : 0 ≤ s) (h : 1 < s ^ n * Real.exp (↑n * q)) : expAtom q < s

Upper certificate: 1 < s ^ n · exp (n·q) gives expAtom q < s.