Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08
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.

Weighted norm invariance for the inversion generator

Statement

For w=(01−10)∈K, one has w⋅z=−1/z and j(w−1,z)=z. Thus at n=2, π2(w)f(z)=z−2f(−1/z)=(−z)−2f(−1/z). For every f∈H2+ this is a bijective isometry of H2+; explicitly, substituting z=−1/u in its squared norm cancels the factor ∣u∣4 from ∣z∣−4 against the real Jacobian ∣u∣−4.

Facts & Assumptions

Given: The Axiom of Choice and the model, norm and action conventions of Holomorphic and antiholomorphic discrete-series models.

[F1]

The fractional maps g⋅z=az+bcz+d and j(g,z)=cz+d define the model action of Holomorphic and antiholomorphic discrete-series models; the matrix identities used below are verified directly in step 1.1.

[F2]

The derivative of z↦−1/z is z−2, and its real Jacobian determinant is the squared modulus of that derivative (Linearity, product, reciprocal, and quotient rules for complex derivatives, The Jacobian determinant of a holomorphic map is ∣f′∣2 and is positive exactly where f′≠0).

[F3]

Nonnegative Lebesgue integrals transform under a C1 diffeomorphism (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F4]

H2+ is the Hilbert space with squared norm ∫H∣f(z)∣2dx dy, and the model formula defines a group action on it (The weighted discrete-series space is a Hilbert space with K-type basis, Holomorphic and antiholomorphic discrete-series models).

[F5]

The same automorphy/Jacobian cancellation is the n=2 case of the general weighted invariance calculation (The weighted area form is SL2(R)-invariant).

[A1]

AC implies Countable Choice, as required by [F3] (The Axiom of Choice, The Axiom of Countable Choice (ACω), AC supplies the countable and dependent choices used in Banach integration).

Proof

technique · direct

Given: f∈H2+ and the matrix w of the Statement.

1.1F1F4algebra

Direct matrix multiplication gives w2=−I and w−1=(0−110), so w⋅z=−1/z and j(w−1,z)=z. Since w−1⋅z=−1/z and j(w−1,z)=z, the model action is π2(w)f(z)=z−2f(−1/z). The map z↦−1/z is an involutive C1 diffeomorphism of H, so this formula defines a holomorphic function there.

1.2F2F3F4algebraA1

Apply [F3] to z=−1/u. By [F2], dAz=∣u∣−4dAu, while ∣z−2∣2=∣u∣4; hence ∥π2(w)f∥22=∫H∣u∣4∣f(u)∣2∣u∣−4dAu=∥f∥22. The integrand is nonnegative, so the change-of-variables identity also holds as an extended integral; for f∈H2+ it is finite.

2.1F1F4F5step 1.2∎

Since w2=−I and the scalar automorphy factor of −I at weight 2 is (−1)−2=1, the group law in [F4] gives π2(w)2=I. Therefore the norm-preserving map of step 1.2 is onto and is a bijective linear isometry. The cancellation is the special n=2 instance of [F5], where the density weight is y0=1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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