ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The modular function of the affine group of the line

Example

Assume the Axiom of Choice (The Axiom of Choice).

Let $G : = {(a, b) : a > 0, b \in R}$ with the multiplication $(a, b) (a^{'}, b^{'}) = (a a^{'}, b + a b^{'}),$ the connected component of the identity of the affine group of the line. Then $d μ = a^{- 2} d a d b$ is a left Haar measure on $G$ , and the modular function of $G$ with respect to it is $Δ_{G} (a, b) = a^{- 1} .$ Since $a \mapsto a^{- 1}$ is not identically $1$ , the group $G$ is nonunimodular (Unimodular locally compact group).

Facts & Assumptions

Given: The group $G = (0, \infty) \times R$ with $(a, b) (a^{'}, b^{'}) = (a a^{'}, b + a b^{'})$ , the measure $d μ = a^{- 2} d a d b$ on it, and AC.

[F1]

$G$ is a group with identity $(1, 0)$ and inverse $(a, b)^{- 1} = (a^{- 1}, - b / a)$ ; it is an open subset of $R^{2}$ , hence an LCH space for the subspace topology, and multiplication and inversion are continuous (Group and abelian group, Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space).

[F2]

A left Haar measure on an LCH group is a nonzero Borel measure that is left invariant, finite on compact sets, outer regular on Borel sets and inner regular on open sets (Left Haar integral and left Haar measure, Radon measure on an LCH space).

[F3]

With $c (g)$ the unique scalar with $\int_{G} F (x g) d μ (x) = c (g) \int_{G} F d μ (x)$ for every nonnegative Borel $F$ and every $μ$ -integrable complex $F$ , the modular function is $Δ_{G} (g) = c (g^{- 1})$ , and $G$ is unimodular exactly when $Δ_{G} \equiv 1$ (Modular function of a locally compact group, Unimodular locally compact group, Right translation scales left Haar measure).

[F4]

Under countable choice (in particular under AC), a $C^{1}$ diffeomorphism $T : U \to V$ between open subsets of $R^{2}$ satisfies $\int_{V} f (y) d y = \int_{U} f (T x) ∣ \det D T (x) ∣ d x$ for nonnegative Lebesgue measurable $f$ (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ ).

[F5]

$a^{- 2} d a d b$ denotes the measure $E \mapsto \int_{E} a^{- 2} d a d b$ given by the Lebesgue density $a^{- 2} > 0$ on the open set $(0, \infty) \times R$ , and every nonempty open subset of $G$ has strictly positive $μ$ -measure.

[A1]

AC is assumed in the choice-function form of the cited definition; it entails the countable choice under which [F4] is stated, and it underlies the well-definedness of the modular function quoted in [F3] (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Verification

technique · direct

1.1

$d μ = a^{- 2} d a d b$ is a nonzero Borel measure, finite on compact sets: on a compact $K \subseteq G$ the continuous density $a^{- 2}$ attains a maximum, so $μ (K) \leq \max_{K} a^{- 2} \cdot λ_{2} (K) < \infty$ , while every nonempty open set has positive measure by [F5]. The rational rectangles contained in $G$ form a countable base, so $G$ is second countable. Under the countable choice implied by [A1], the compact-finite Borel measure $μ$ is outer regular on Borel sets and inner regular on open sets by Locally finite Borel measures on second-countable LCH spaces are regular.

A1F1F2F5

1.2

Left invariance. Fix $g_{0} = (a_{0}, b_{0}) \in G$ . Left multiplication is $L_{g_{0}} (a, b) = (a_{0} a, b_{0} + a_{0} b)$ , a $C^{1}$ diffeomorphism of $G$ with $\det D L_{g_{0}} = a_{0}^{2}$ at every point. For nonnegative Borel $F$ , the change of variables [F4], whose countable-choice hypothesis is in force by [A1], applied to $(u, v) = L_{g_{0}} (a, b)$ gives $\int_{G} F (L_{g_{0}} (a, b)) a^{- 2} d a d b = \int_{G} F (u, v) (u / a_{0})^{- 2} a_{0}^{- 2} d u d v = \int_{G} F (u, v) u^{- 2} d u d v$ , since the inverse map is $a = u / a_{0}$ , $b = (v - b_{0}) / a_{0}$ and $∣ \det D L_{g_{0}}^{- 1} ∣ = a_{0}^{- 2}$ . Hence $μ$ is left invariant.

A1F4F5

1.3

Right translation scales $μ$ by $a_{0}$ . With the same $g_{0}$ , right multiplication is $R_{g_{0}} (a, b) = (a a_{0}, b + a b_{0})$ , a $C^{1}$ diffeomorphism with $\det D R_{g_{0}} (a, b) = \det (\begin{array}{cc} a_{0} & 0 \\ b_{0} & 1 \end{array}) = a_{0}$ . For nonnegative Borel $F$ , the change of variables [F4], again in force by [A1], with $(u, v) = (a a_{0}, b + a b_{0})$ gives $\int_{G} F (a a_{0}, b + a b_{0}) a^{- 2} d a d b = \int_{G} F (u, v) (u / a_{0})^{- 2} a_{0}^{- 1} d u d v = a_{0} \int_{G} F (u, v) u^{- 2} d u d v$ , using $a = u / a_{0}$ , $b = v - (u / a_{0}) b_{0}$ and $∣ \det D R_{g_{0}}^{- 1} ∣ = a_{0}^{- 1}$ . So $\int_{G} F (x g_{0}) d μ (x) = a_{0} \int_{G} F d μ$ for every nonnegative Borel $F$ , and also for every $μ$ -integrable $F$ by linearity in the real and imaginary parts.

A1F4F5

2.1

The scalar of step 1.3 is $c (g_{0}) = a_{0}$ , so $Δ_{G} (g_{0}) = c (g_{0}^{- 1})$ , the scalar $c (g_{0}^{- 1})$ being the well-defined one supplied under the AC of [A1]; applying step 1.3 to $g_{0}^{- 1} = (a_{0}^{- 1}, - b_{0} / a_{0})$ gives $c (g_{0}^{- 1}) = a_{0}^{- 1}$ . Hence $Δ_{G} (a_{0}, b_{0}) = a_{0}^{- 1}$ for every $(a_{0}, b_{0}) \in G$ , which is the asserted modular function.

A1F3step 1.3

3.1

The function $(a, b) \mapsto a^{- 1}$ is not identically $1$ on $G$ : at $(2, 0)$ it takes the value $1 / 2$ . By [F3] the group $G$ is therefore not unimodular, while steps 1.1–1.2 show that $a^{- 2} d a d b$ is indeed a left Haar measure for which the computation of step 2.1 applies. ∎

F3step 1.1step 1.2step 2.1

Verification notes

Why the positive component. The full affine group ${a \neq 0}$ has two components and its connected component of the identity is the $a > 0$ part treated here, which avoids a disconnected sign convention for the modular function.
Choice cost. AC is declared as [A1]; its countable-choice consequence is used in steps 1.2 and 1.3 through the change-of-variables theorem [F4], and it underlies the well-definedness of the scalar $c (g)$ quoted from [F3] in step 2.1. The Jacobian computations, the density $a^{- 2}$ and the nonunimodularity witness are choice-free.

Depends on

Used by

Naive inversion is not the L1 involution on a nonunimodular group Counterexample

Dependency tree · two levels

53 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Bekka, de la Harpe and Valette, Kazhdan’s Property (T), Appendix A §§A.3–A.4 (standard reference, not scraped)
Emmanuel Kowalski, Representation Theory of Groups, §§5.2–5.3 (standard reference, not scraped)