Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
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.

Continuum contribution in perturbation

Example

Assume Countable Choice (The Axiom of Countable Choice (ACω)), as required by the analytic coefficient supplier. Let H:=C⊕L2((1,2),dx;C) with norm ∥c⊕f∥2=∣c∣2+∫12∣f∣2dx and inner product linear in the first variable (Hilbert space, The space Lp(μ) as the quotient by null functions). Let H0:=0⊕Mx on all of H, with Mxf(x)=xf(x). The operator is bounded and self-adjoint, with spectrum {0}∪[1,2]; E=0 is an isolated simple eigenvalue with gap g=1. These assertions and its concrete PVM are verified directly below, without a general AC spectral theorem. Define V(c⊕f):=(∫12f(x)dx)⊕c1(1,2). This example verifies that:

(a) V is bounded and self-adjoint, with ∥V∥=1. P0(c⊕f)=c⊕0 is the projection onto C⊕{0}, and ψ0:=1⊕0 is a unit vector with ⟨Vψ0,ψ0⟩=0.

(b) With Q=I−P0, HQ=H0∣QH=Mx and the actual reduced inverse S=ιQ(HQ−E)−1Q=0⊕M1/x, the second-order coefficient of Simple-level reduced-resolvent coefficients is exactly E′′(0)2=−⟨VSVψ0,ψ0⟩=−∫12dxx=−log⁡2<0. The coefficient theorem applies for all complex ∣λ∣<1/4, where q=2∣λ∣<1/2; the first-order coefficient is zero. The contour supplier applies on the larger disk ∣λ∣<1/2.

(c) The entire second-order coefficient comes from the continuous, indeed absolutely continuous, complementary spectrum of H0 on [1,2]. A bound-state-only sum returns 0, so it misses this nonzero complementary contribution.

Verification

Given: CC, the concrete H,H0,V,P0,Q,S,ψ0 above and the first-variable-linear pairing.

[F1] Projection valued measure, A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Hilbert space and The space Lp(μ) as the quotient by null functions specify the operators, quotient classes and Hilbert norm. Under the assumed Countable Choice, Complex completeness, density, and inner product: the consumer interface gives completeness and the first-variable-linear pairing for complex L2 on every measure space; apply it to Lebesgue measure on (1,2). Multiplication by bounded measurable functions preserves these quotient classes; Cauchy-Schwarz inequality for L2 bounds the scalar integral in V, and Dominated convergence gives the strong convergence of indicator-multiplier tails.

[F2] Simple-level reduced-resolvent coefficients, with the actual restricted inverse on QH, gives E′(0)=⟨Vψ0,ψ0⟩ and E′′(0)/2=−⟨VSVψ0,ψ0⟩ under CC and q<1/2. Contour perturbation projection gives the holomorphic simple eigenvalue on q<1. The example verifies all operator, spectral, normalization, gap and perturbation hypotheses locally before using them.

[F3] The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t identifies ∫12dx/x=log⁡2. Positivity is also immediate from 1/x>0 on a positive-length interval.

1.1F1givenalgebra

[Explicit operator and spectral measure] The L2((1,2)) completeness and pairing in [F1] make it a complex Hilbert space. If cn⊕fn is Cauchy in the stated direct-sum norm, each component is Cauchy; completeness of C and this L2 space gives limits c,f, and the norm identity gives convergence to c⊕f. Thus H is complete before any Hilbert-space theorem or PVM definition is used. Since 1<x<2, Mx is bounded on all L2(1,2) with norm 2, and real multiplication gives ⟨Mxf,h⟩=⟨f,Mxh⟩. A bounded symmetric operator on the whole Hilbert space equals its adjoint directly by the defining pairing, so H0 is self-adjoint with domain H. For every real Borel B define E(B)(c⊕f)=1B(0)c⊕1B(x)f(x). These are orthogonal projections, E(R)=I, and their products are E(B∩C). On a fixed vector, disjoint countable additivity follows from pointwise indicator sums and the integrable squared-norm majorant ∣f∣2 (with the scalar component evaluated at 0), so this is a PVM. Its scalar measures are ∣c∣2δ0(B)+∫B∩(1,2)∣f(x)∣2dx. Integrating bounded simple approximations to the coordinate function on {0}∪[1,2] yields H0=∫t dE(t) on all H. Thus the representing PVM and its bounded multiplier realization are explicit.

2.1step 1.1F1algebra

[Spectrum, gap and absence of complementary eigenvectors] For z∉{0}∪[1,2], (z−H0)−1(c⊕f)=c/z⊕f/(z−x) is a bounded two-sided inverse on H. For any t∈[1,2] and ε>0, the interval J=(1,2)∩(t−ε,t+ε) has positive length. The vector 0⊕1J/∣J∣1/2 is unit and has ∥(H0−t)u∥≤ε, excluding a bounded inverse at t. Finally ker⁡H0=C⊕{0}, so 0 is an isolated simple eigenvalue and its distance to the remaining spectrum is g=1. The equation (x−t)f=0 forces f=0 in L2(1,2) because a singleton has Lebesgue measure zero. Consequently the complementary block has no eigenvectors and all its spectral measures are absolutely continuous with densities ∣f∣2 on (1,2), including zero atom at the endpoints. In particular P0=E({0}) and ψ0=1⊕0 has norm one.

3.1step 1.1step 2.1F1F2algebra

[Perturbation hypotheses and the restricted inverse] Let I(f)=∫12f(x)dx=⟨f,1⟩. Cauchy-Schwarz and the interval's length one give ∣I(f)∣≤∥f∥2. Therefore ∥V(c⊕f)∥2=∣I(f)∣2+∣c∣2≤∥c⊕f∥2; equality at ψ0 gives v=∥V∥=1>0. For c⊕f,d⊕h, the first-variable-linear pairing gives ⟨V(c⊕f),d⊕h⟩=I(f)d‾+cI(h)‾=⟨c⊕f,V(d⊕h)⟩, so V=V∗. Moreover Vψ0=0⊕1 and the first-order pairing is zero. On QH=0⊕L2(1,2), HQ−E=Mx has inverse M1/x, bounded on that exact whole complementary domain with norm one. Hence S(c⊕f)=0⊕(f/x), SP0=P0S=0 and (H0−E)S=S(H0−E)=Q on H. No global inverse of H0−E is used. The preceding operator, spectral and perturbation computations verify every concrete hypothesis of [F2], with inherited CC and q=2∣λ∣.

4.1step 1.1step 2.1step 3.1F2F3algebra∎

[Exact coefficient and its continuous origin] The explicit reduced inverse gives SVψ0=0⊕(1/x) and VSVψ0=(∫12dx/x)⊕0. Pairing with the unit ψ0 and applying [F2], [F3] yields E′′(0)/2=−∫12dx/x=−log⁡2<0. The scalar spectral measure of Vψ0=0⊕1 is exactly 1(1,2)(x)dx by step 1.1, so the entire coefficient integrates 1/x over the continuous complementary spectrum. Step 2.1 shows that the only bound eigenvector belongs to P0H, with zero coupling matrix element; there are no complementary bound eigenvectors. A sum restricted to bound states therefore gives zero and omits the exact negative coefficient. This proves all original example claims, its normalization and class, with the correct restricted inverse and explicit inherited CC.

Depends on

Dependency tree · 2 levels

Sources