Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
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.

A boundary flux control uses the H1 trace and a different control operator

Statement

Assume the Axiom of Choice. For Ω=(0,1), realize V=H1(0,1) by its unique absolutely continuous representatives, with norm ∥v∥V=(∥v∥22+∥v′∥22)1/2. For a smooth state satisfying −u′′+u=f, u′(0)=0, and u′(1)=g, integration by parts gives the weak boundary load v↦gv(1). The boundary control parameter is a scalar, equivalently L2({1}) for counting measure. For g≠0, its trace functional is not representable by an interior density q∈L2(0,1); for g=0, both loads include the zero functional. Thus the boundary control space and its trace operator must be specified separately from the distributed-control space L2(0,1).

Facts & Assumptions

Given: The Axiom of Choice, the interval, the energy space H1(0,1), and the one-dimensional weak formulation of a Neumann boundary load.

[A1]

The Axiom of Choice is assumed (The Axiom of Choice).

[F1]

The control box Closed pointwise box of L2 controls consists of equivalence classes in an L2 space over its declared measure domain; changing the domain changes the control space.

[F2]

Under the Axiom of Choice, every H1(0,1) class has a unique absolutely continuous representative on [0,1] (One-dimensional W1,p functions have unique absolutely continuous representatives).

[F3]

The Axiom of Choice implies Dependent Choice and Countable Choice (AC implies DC implies countable choice).

[F4]

For absolutely continuous functions, integration by parts gives ∫FG′+∫F′G=F(1)G(1)−F(0)G(0) when Countable Choice and Dependent Choice hold (Integration by parts for absolutely continuous functions).

[F5]

Cauchy--Schwarz gives ∣∫01ab∣≤∥a∥2∥b∥2 (Cauchy–Schwarz: ∣⟨x,y⟩∣≤∥x∥ ∥y∥, with equality exactly for dependent pairs).

Verification

1.1A1F2F3F4F5givenalgebra

By [F2], v has an absolutely continuous representative. By [F3], the hypotheses of [F4] hold. Applying [F4] to F(x)=x and G(x)=v(x) gives v(1)=∫01v(x) dx+∫01xv′(x) dx. Cauchy--Schwarz [F5] yields ∣v(1)∣≤∥v∥2+∥v′∥2≤2∥v∥V. Applying [F4] to F=u′ and G=v for a smooth state gives ∫01(u′v′+uv) dx=∫01fv dx+gv(1). Thus the boundary control operator B∂g:v↦gv(1) is bounded on V.

2.1F1F5step 1.1givenalgebra∎

Let vn(x)=max⁡{1−n(1−x),0}. Then vn∈H1(0,1), vn(1)=1, and ∥vn∥2=(3n)−1/2. If g≠0 and gv(1)=∫01qv for every v∈V with some q∈L2(0,1), Cauchy--Schwarz [F5] gives ∣g∣=∣∫01qvn∣≤∥q∥2(3n)−1/2→0, a contradiction. For g=0, q=0 represents the same zero functional. The boundary input space is nevertheless the scalar L2({1}) space, while the distributed input space in [F1] is L2(0,1); their operators and control sets must be specified separately.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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