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.
Constant-field branch on a ball
Example
Let be the open Euclidean ball of radius , regarded as an oriented smooth three-manifold without boundary, and let . Here means that all partial derivatives of every finite order on extend continuously to . For a fixed with units of inverse length, prescribe smooth contravariant fields , , and , ; both are restrictions of smooth maps on . Set , , so and both barred fields have zero Euclidean divergence. For every sufficiently small , the local Dirichlet branch gives a function with and
With , , , and , the conformal formulas , , , and define smooth constrained electrovacuum initial data on ; here time-symmetric means , and constrained means satisfying both Maxwell divergence constraints and the Hamiltonian and momentum constraints. The boundary condition is prescribed data on this fixed ball; this is not an isolated asymptotically flat black-hole construction.
Example references
Small charged Dirichlet conformal branch
Conformal electrovacuum seed data
Exact conformal electrovacuum constraint transformation
Constrained electrovacuum initial data
Local energy and zero-boundary closure for the charged constraint problem
Higher-order boundary regularity for Dirichlet problems
Facts & Assumptions
Given: , , the prescribed seed fields and their -scaled barred fields from the Example, and the Axiom of Choice and Countable Choice.
The Axiom of Choice and Countable Choice are assumed by the small-branch theorem, the Sobolev embedding/algebra suppliers, and the higher-order regularity route. The Axiom of Choice The Axiom of Countable Choice ()
Bounded-domain charged conformal problem: is nonnegative, has zero boundary values, and with .
Small charged Dirichlet conformal branch: for sufficiently small , there is a locally unique branch with and , where and on the boundary.
Conformal electrovacuum seed data: , , and , for smooth seed fields on the three-manifold.
Exact conformal electrovacuum constraint transformation: the barred Maxwell constraints are ; the transformed Hamiltonian equation includes when , , and ; the momentum equation is satisfied when and .
Constrained electrovacuum initial data: constrained data satisfy the two Maxwell divergence equations, the Hamiltonian scalar equation, and the momentum covector equation displayed in that definition.
Local energy and zero-boundary closure for the charged constraint problem: a function with zero boundary restriction belongs to .
Integer-order Sobolev spaces and their norms and Weak Dirichlet solutions for a divergence-form operator: records square-integrable weak derivatives through order ; a zero-boundary weak solution of satisfies for every .
Higher-order boundary regularity for Dirichlet problems: on a bounded smooth domain, a zero-trace weak solution of lies in .
Higher-order Sobolev embedding: under the Axiom of Choice, on a bounded -extension domain in dimension three, for , for , and whenever and ; The Sobolev space is an algebra above the critical index: on such a domain, is a Banach algebra for .
Ambient smooth restrictions are dense on bounded C^k domains: restrictions of ambient compactly supported smooth functions are dense in for each finite integer .
The chain rule for total derivatives: : the total derivative of a differentiable composition is the composition of the total derivatives; iteration gives the finite chain rule for the smooth approximants used below.
A bounded domain means a nonempty bounded open set locally on one side of a boundary graph. Under the Axiom of Choice, every such domain admits a bounded linear operator with almost everywhere, for each integer ; this is precisely the -extension-domain hypothesis in [F9]. No common operator for all is needed. Bounded C^k domains and boundary charts Sobolev extension domains and extension operators Bounded C^k domains admit integer-order Sobolev extension
Verification
The base fields are smooth and , so the source in [F1] is the constant , and scaling them by preserves their zero divergences. The units are consistent: and have units of inverse length squared, while and are dimensionless. At any point of , rotate that point to . In a sufficiently small neighborhood its boundary is and the ball occupies the side below this graph. The graph is smooth for , so the ball is a bounded domain for every finite . By [A1] and [F12] it is a -extension domain for each ; all uses of [F9] below therefore meet that hypothesis.
Smoothness bootstrap, initial gain. Set and , so and on . The branch gives and . The identities and follow from [F11] and the product rule and show that , with bounded derivatives through order two, hence by integration by parts against compactly supported tests. By [F6], . Its classical equation tested against gives the weak identity; continuity of both sides in the test norm and the defining density of in extend it to every test in . Applying [F8] with yields .
On , define . It vanishes on , and in , so . By uniqueness of the zero-boundary solution in [F2], this is the coefficient in the branch expansion.
Smoothness bootstrap, composition and iteration. Fix an integer and suppose . Its continuous range is a compact interval by [F2] and [F9]. To verify , use [F10] to choose smooth restrictions in ; [F9] gives uniform convergence, so for all sufficiently large the values of lie in one compact interval containing . For each smooth with values in , repeated application of the total chain and product rules [F11] expresses every , , as a finite sum of bounded factors , , times products with and . Each product is in with a bound controlled by : derivatives of order at most lie in or a higher Sobolev space and hence in by [F9]; a factor of order can occur only alone and is in ; a factor of order occurs at most once, lies in , and any remaining factor has total derivative order at most one and lies in . Thus is uniformly bounded in on the bounded smooth approximants and their line segments. The same difference identity applied to shows is continuous in , so its displayed integral exists as a Banach-valued Riemann integral. The identity , together with the Banach-algebra bound [F9], shows is Cauchy in . Its uniform limit is , proving . Hence ; [F8] gives . Starting with and repeating for proves for every sufficiently large integer . The same embeddings imply for every finite integer , and then for every , so .
Verification of the full constraints. On the oriented manifold without boundary , take the conformal seed data , , , , , and . Smoothness and positivity of follow from steps 1.2–2.2 and [F2], so [F3] defines smooth and gives . The Maxwell constraints hold because by step 1.1 and the barred metric is Euclidean. Since and , the transformed Hamiltonian constraint [F4] is exactly , the branch equation. Its transformed momentum equation has zero left side because and zero right side because . Thus all four constraints in [F5] hold. The data are smooth constrained time-symmetric data on this fixed ball; the Dirichlet boundary value is prescribed, and the proof makes no claim of an isolated asymptotically flat black hole or any other boundary-value problem.
Depends on
Small charged Dirichlet conformal branch
Bounded-domain charged conformal problem
Conformal electrovacuum seed data
Exact conformal electrovacuum constraint transformation
Constrained electrovacuum initial data
Local energy and zero-boundary closure for the charged constraint problem
Higher-order boundary regularity for Dirichlet problems
Higher-order Sobolev embedding
The Sobolev space is an algebra above the critical index
Ambient smooth restrictions are dense on bounded C^k domains
Integer-order Sobolev spaces and their norms
Weak Dirichlet solutions for a divergence-form operator
The chain rule for total derivatives:
The Axiom of Choice
The Axiom of Countable Choice ()
Bounded C^k domains admit integer-order Sobolev extension
Sobolev extension domains and extension operators
Bounded C^k domains and boundary charts
Dependency tree · 2 levels
Sources
- A. I. Alcubierre, J. C. Degollado and M. Salgado, The Einstein-Maxwell system in 3+1 form and initial data for multiple charged black holes, arXiv:0907.1151v2 (2009)
- David Gilbarg and Neil S. Trudinger, Elliptic Partial Differential Equations of Second Order (2001)
- John K. Hunter, Notes on Partial Differential Equations (2014)
- Juha Kinnunen, Sobolev Spaces (2026)
- J. Lebl, Basic Analysis I
- Sung-Jin Oh, Lecture Notes for Math 222A (2024)