text:
# Computer theorem proving in math

## 1. Introduction

When I was taking Wilfried Schmid’s class on variations of Hodge structure, he came in one day and said “ok, today we’re going to calculate the sign of the curvature of the classifying space in the horizontal directions”. This is of course the key point in the whole theory: the negative curvature in these directions leads to all sorts of important things such as the distance decreasing property.

So Wilfried started out the calculation, and when he came to the end of the first double-blackboard, he took the answer at the bottom right and recopied it at the upper left, then stood back and said “lets verify what’s written down before we erase it”. Verification made (and eventually, sign changed) he erased the board and started in anew. Four or five double blackboards later, we got to the answer. It was negative.

Proof is the fundamental concept underlying mathematical research. In the exploratory mode, it is the main tool by which we percieve the mathematical world as it really is rather than as we would like it to be. Inventively, proof is used for validation of ideas: one uses them to prove something nontrivial, which is valid only if the proof is correct. Other methods of validation exist, for example showing that an idea leads to computational predictions—but they often generate proof obligations too. Unfortunately, the need to prove things is the factor which slows us down the most too.

It has recently become possible, and also necessary, to imagine a full-fledged machine-verification system for mathematical proof. This might radically change many aspects of mathematical research—for better or for worse is a matter of opinion. At such a juncture it is crucial that standard pure mathematicians participate.

The present paper is intended to supply a synthetic contribution to the subject. Most, or probably all, is not anything new (and I take this opportunity to apologize in advance for any additional references which should be included). What is supposed to be useful is the process of identifying a certain collection of problems, and some suggestions for solutions, with a certain philosophy in mind. The diverse collection of workers in this field provides a diverse collection of philosophical perspectives, driving our perception of problems as well as the choice of solutions. Thus it seems like a valid and useful task to set out how things look from a given philosophical point of view. Our perspective can be summed up by saying that we would like to formalize, as quickly and easily as possible, the largest amount of standard mathematics, with the ultimate goal of getting to a point where it is concievable to formalize current research mathematics in any of the standard fields.

This is a good moment to point out that one should not wish that everybody share the same point of view, or even anything close. On the contrary, it is good to have the widest possible variety of questions and answers, and this is only obtained by starting with the widest possible variety of philosophies.

We can now discuss the difference between what we might call “standard” mathematical practice, and other currents which might be diversely labelled “intuitionist”, “constructivist” or “non-standard”. In the standard practice, mathematicians feel free to use whatever system of axioms they happen to have learned about, and which they think is currently not known to be contradictory. This can even involve mixing and matching from among several axiom systems, or employing reasoning whose axiomatic basis is not fully clear but which the mathematician feels could be fit into one or another axiomatic system if necessary. This practice must be viewed in light of the role of proof as validation of ideas: for the standard mathematician the ideas in question have little, if anything, to do with logical foundations, and the mathematician seeks proof results for validation—it is clear that any generally accepted framework will be adequate for this task.

A growing number of people are interested in doing mathematics within an intuitionist or constructive framework. They tend to be closest to mathematical logic and computer programming, which may be why many current computer-proving tools are to some degree explicitly designed with these concerns in mind. There are many motivations for this, the principal one being deeply philosophical. Another is just concern about consistency—you never know if somebody might come up with an inconsistency in any given axiomatic system (see  for example). Common sense suggests that if you take a system with less axioms, there is less chance of it, so it is possible to feel “safer” doing mathematics with not too many axioms. A subtler motivation is the question of knowing what is the minimal axiomatic system under which a given result can be proven, see  for example. Computer-scientists have some wonderful toys which make it possible directly to transform a constructive proof into a computational algorithm.

The problem of computer-verified-proof in the standard framework is a distinct major goal. Of course, if you prove something in a constructive framework, you have also proven it in the standard framework but the opposite is not the case. Integrating additional axioms such as replacement or choice into the theory, gives rise to a distinct optimization problem: it is often easier to prove a given thing using the additional axioms, which means that the structure of the theory may be different. The notion of computer verification has already made important contributions in many areas outside of “standard” mathematics, and it seems reasonable to think that it should also provide an important tool in the standard world.

One could also note that, when you get down to the nitty-gritty details, most technical results concerning lambda calculus, including semantics, normalization and consistency results for various (highly intuitionistic) axiomatic systems, are themselves proven in a standard mathematical framework relying on Zermelo-Frankel set theory (see  for example). Thus even people who are interested in the intuitionist or constructive side of things might find it useful to have good standard tools at their disposal.

One reason why computer theorem verification in the standard pure mathematical context is not recieving enough attention is that most pure mathematicians are unaware of the subject. This lack of awareness—which I shared a few years ago—is truly colossal, given the literally thousands of papers concerning the subject which have appeared in recent years. Thus it seems a bit silly, but one of the goals of the present paper is to try to spread the news.

This ongoing work is being done with a number of other researchers at Nice: A. Hirschowitz, M. Maggesi, L. Chicli, L. Pottier. I would like to thank them for many stimulating interactions. The referee kindly pointed out the references  and , and several readers of the first version sent helpful remarks and references. I would like to thank C. Raffalli, creator of the PhoX system, who explained some of its ideas during his visit to Nice last summer—these have been very helpful in understanding how to approach proof documents. Special thanks are extended to the several members of the Coq group at INRIA, Rocqencourt, for their continuing help during visits and on the mailing list. From much further past, I would like to thank M. Larsen for teaching me what little I know about computer programming.

I would like warmly to thank S. Gutt for organizing a great conference, for letting me give a talk which was fairly widely off-subject, and for suggesting a title. And of course the birthday-teenagers for reminding us of the Sumerian numbering system .

## 2. Basic reasons

The basic goal of mechanized theorem verification is to have a language for creating mathematical documents, such that the reasoning can be checked by computer.111We ask that the machine verify the proofs supplied by the mathematician; obviously it can help if the machine finds the proof on its own but that constitutes a difficult, and somewhat distinct, research problem . This is of interest to pure mathematicians for reasons such as the following.

2.1—To reduce the number of mistakes we make in our mathematical work (there are lots of them! ).

2.2—Dealing with complicated theories—it is difficult to manage development when there are too many things to prove (and often the author doesn’t even know exactly what it is he needs to check).

2.3—Because of (2.1) and (2.2), nobody really has the time or energy adequately to verify all new results, which leads to problems for publication or other timely dissemination. If articles could be validated by machine then referees could concentrate on the question of how interesting they are.

2.4—Black-box theories: it is sometimes useful, but currently dangerous, to use results without knowing how they are proven. An author can have a certain situation in mind, and might use arguments which work in that situation but not in other ones, but sometimes the explicit statements of results don’t adequately reflect all the hypotheses. So future users need to understand the arguments before blindly applying the statements. An advantage of machine verification is that the language has to be totally precise: utilization of a “black box” via cut-and-paste rather than axiomatically leaves no room for misinterpretation.

2.5—Integration of many theories or points of view: it is hard for humans because of the steep learning curve for each new theory. Even now the importation of techniques, without a full understanding of how they work, is a little-heralded part of mathematical practice, generally glossed over because of the problems of accuracy that are posed. With machine-verified proving these problems should in large part be resolved and should lead to a much more diverse fabric in which different workers develop different techniques and import the techniques of others without needing to spend such a long time learning about the details, leaving everyone with more energy to spend looking for new ideas.

2.6—New forms of reasoning: now, calculations or proofs with little motivation are ruled out by the fact that the mathematician needs to be motivated in order to understand what is going on. Locally unmotivated reasoning might lead to globally interesting results. A striking example in logic is work on minimal length axioms such as  , where much of the reasoning was found using theorem-proving software.

2.7—The advent of more and more proofs making use of computer calculation (non-existence of a projective plane of order $`10`$  , the 4-color theorem, more recently a theorem on hyperbolicity of $`3`$-manifolds  and the Kepler conjecture ) represents a priori a somewhat different use of the computer than what we are considering here. However, these proofs pose acutely the problem of verifying logical details, and a formalized framework promises to present a significant improvement. This issue was addressed by B. Werner in a talk at Nice about the 4-color theorem, and has motivated Hales’ “flyspeck project” .

2.8—The possibility of computer-assisted proof verification would significantly extend the age period in which mathematicians are optimally productive: older mathematicians tend to avert getting bogged down in details, which often prevents full development of the continuing stream of valid ideas.

On the whole, it is a mistake to think that computer theorem-proving will always lag behind regular math. At some point, the advantages will so much more than counterbalance the difficulties that mathematicians using these tools will jump out ahead.

## 3. History

3.1—Cantor, Hilbert, Russell; then Gödel and so on, worked on providing a strict logical foundation for mathematics.

Church, Rosser, Martin-Löf , Girard  worked more specifically on the logical foundations of type theory.

3.2—Automath, the project of de Bruijn, was one of the first explicit projects in this direction; notably he pointed out how to deal with variables (via de Bruijn indices).

In 1977, Jutting entered all of Landau’s analysis book in the AUTOMATH system .

3.3—The first long-term project involving a very large number of people was Mizar; it is still ongoing, and led to the Journal of Formalized Mathematics which has been publishing articles verified in the MIZAR system since at least 1989. This includes much basic theory but also research articles. The mathematical orientation of the research articles is sometimes distinguished from the mainstream of what we call standard mathematics (this is an observation but not a criticism).

3.4—More recently, a number of systems based on some kind of type theory have been developped: HOL, Lego, Isabelle, Nuprl, Nqthm, AC2L, and general “Boyer-Moore” theorem provers…

Coq is a project which seems relatively successful with respect to the considerations discussed below.

An overview of very recent systems would include: Elf, Plastic, Phox, PVS, IMPS, Ghilbert, Metamath. These and many more can be found using an internet search engine—a little perseverance turns up an astounding amount of reference material which we couldn’t begin to include here (and which is impossible to read in its entirety). A good place to start is with meta-pages such as , .

3.5—Industrial demand, spurred in part by some well-known problems that might have been avoided with use of the appropriate proof technology (Pentium, Ariane 5), continues to be a major impetus for the development of proof engines. In this case, interest is oriented toward proving the correctness of algorithms, integrated circuits or other wiring diagrams, and so forth.

3.6—More and more conferences, journals, and mailing lists bear witness to the fact that fields related to computer proof verification are really booming. Browsing the archives of mailing lists such as  or  is a fascinating homework assignment.

3.7—In contrast we might mention that the notion of computer calcuation systems, which is perhaps much better known in the world of pure mathematics, is not quite the same thing as computer proof verification. It is surely related, though, and is also experiencing fast growth. Idem for the closely related field of automated deduction (see  for a survey).

3.8—Some recent examples of proof developments which are of interest to the pure mathematician are: the fundamental theorem of algebra, by Geuvers et al ; R. O’Connor’s formalization of Gödel’s theory ; the `Reals` and other recent libraries for Coq ; L. Chicli’s thesis about algebraic geometry ; the logical libraries in Isabelle ; Metamath’s work on Hilbert spaces , ….

A glance at this history leads to the conclusion that it now seems like all of the ingredients are available so that we could start doing computer theorem verification in a serious way. We just have to find the right combination. It doesn’t seem unreasonable to think that this moment will be seen, in retrospect, as an important juncture in the history of mathematics.

## 4. Extra-mathematical considerations

It is useful to elucidate some criteria explaining what would make the difference between a system which would or would not be used and accepted by mathematicians. The model of mathematical typesetting and suggests some criteria.

4.1free: the program shouldn’t cost anything (and should be free of any other constraints) for scientific users.

4.2plain text: the main format of the proof document should be a plain text file; this is to insure that nothing is hidden to the user between the document creation and its compilation or verification, and also to insure easy exchange of documents.

4.3open source: the basic programming code used to specify the syntax of the language, and to verify the proof document, should be available to everybody. In the best case it would actually be attached as a trailer to the proof document itself, since the program is an integral part of the proof specification (see the discussion of archiving in the introduction of ). Open source for this key part of the system brings the guarantee that your document will be readable or compilable at any time in the future.

4.4reference manual: it should be possible to get started using only the reference manual, and at the same time the manual should answer even the most arcane questions (first-time users tend to stumble upon arcane questions more often than one might expect, cf ).

4.5cross-platform: it should be very easy to install and use on all platforms. One of the most difficult aspects for a mathematician getting started in this subject is just to get a system up and running usably on whatever computer is available. The average mathematician should be able to install the system and type out a first text file which is then successfully verified, proving a simple mathematical lemma such as uniqueness of the identity element in a monoid, in no more than a couple of hours.

4.6modifiable: the system should be modifiable by the user, in particular the user should choose (or invent, or re-invent) his own axiomatic framework, his notational system, his proof tactics in a fully programmable language, and so on—these things shouldn’t be hard-wired in. In William Gibson lingo, we want something that would give the “Turing police” nightmares. This information would be like the notion of a macro header to a TeX file. People could exchange and copy their header material, but could also modify it or redo it entirely. This is very important for enabling creative research.

4.7encourage mathematicians: the people who maintain the system should encourage standard mathematicians to write math in the system. This includes maintaining an archive, and publicizing the existence of the system within the standard pure mathematical community.

4.8attentiveness to user suggestions: pure mathematicians are the scientists who work the most with proof, and it seems logical that their viewpoints would be important to development of a fully functional system. Input from pure mathematicians is likely to be useful even in more far-flung areas of the subject such as industrial applications. This could be seen as compensation for the requirements that the system be free and open-source.

## 5. Starting tasks

The hardest part of the subject is the first basic task which needs to be addressed: you need to form an opinion about what you are going to want your documents to look like .

This task is of course first and foremost treated by the system designers. However, even within the framework of a given system, the mathematician has to address this task too, in determining the style he will use.

It is subject to a number of constraints and hazards.

5.1—Everything you write down has to have an absolutely well-defined and machine-determinable meaning.

5.2—One must write things in a reasonably economical way, in particular we need a reasonable system of notation for the standard mathematical objects which are going to be manipulated.

5.3—It is better if any difficulties which are encountered, have actual mathematical significance. An example of a difficulty which doesn’t seem to have much real mathematical significance arises in type theory when we have two types `A` and `B`, with an element `a:A` and a known (or supposed) equality `A=B`. It often (depending on the type system being used) requires additional work in order to be able to say that `a:B`. To the extent possible, the pure mathematician will want to choose a format in which any such hurdle is seamlessly cured.

5.4—At least a part of what is written should be comprehensible, preferably upon simple inspection of the pure text file.

5.5potential problem: it is quite possible (and maybe even generally the case) to invent notation which suggests a meaning different from the actual meaning. When you prove a given statement, did you really prove what you thought you did?

Unfortunately there is no way for the computer to verify this part. The conclusion is that we require human comprehension of the definitions, and of the statements of the theorems (the main ones, at least). This imperious requirement is stronger than the natural desire also to understand the proofs.

5.6—Experience suggests that the proofs, in their explicit and verifiable form, actually contain too much information and the reader will not really want completely to understand them. Indeed the origin of the whole project is the fact that we aren’t able to follow the details of our proofs. Rather one might ask that two particular aspects stand out: the general strategy, and the unexpected main steps.

## 6. How it works

We describe in brief some of the salient points of the `Coq v8.0` system  currently used by the author. A number of other recent systems are similar. Aside from the geographical reason for my choice of system, one can point out that `Coq` scores pretty well (but naturally with room for improvement) on the above lists of desiderata. 222If the makers of other systems feel impelled at this point to say “hey, our system does just as well or better”, the main point I am trying to make is: That’s great! Try to get us working on it!

6.1—Some natural considerations lead to the idea of using type theory as a basis for mathematical verification . To start with, notice that we want to manipulate various sorts of objects, first and foremost the mathematical statements themselves. Although perhaps not strictly necessary, it is also very important to be able directly to manipulate the mathematical entities appearing in the statements, be they numbers, sets, or other things. To deal with our entities (which will be denoted by expressions entered into the text file), we need function application `(f x)` and function-definition

```
fun x => (... x ... x ....).

```

This combination of operators yields the lambda calculus. The notion of $`\beta `$-reduction is that if

```
f:= fun x =>(... x ... x ....)

```

then for any expression `y`, the application `(f y)` should reduce to
`(... y ... y ....)`. It is natural to ask that the computer take into account this reduction automatically.

6.2—The first famous difficulty is that if `f:= fun x =>x x` then `(f f)= (fun x =>x x) f` $`\stackrel{\beta }{}`$ `(f f)` $`\stackrel{\beta }{}`$ `(f f)` …. Thus the $`\beta `$-reduction operation can loop.

The solution is the notion of type introduced by Russell: every “term” (i.e. allowable expression, even a hypothetical or variable one) has a “type”. The meta-relation that a term `x` has type `X` is written `x:X`. The $`\lambda `$ construction (construction of functions) is abstraction over a given type: we have to write

```
f:= fun (x:A)=>(... x ... x ....)

```

where `A` is supposed to designate a type. Furthermore the expression on the right is required to be allowable, i.e. well-typed, under the constraint that `x` has type `A`.

6.3The Church-Rosser theorem states that:
In typed $`\lambda `$-calculus, $`\beta `$-reduction terminates; also calculation of the typing relation terminates.

The verification program (such as Coq) basically implements this calculation. The fact that it is sure to terminate is a considerable advantage for the end-user: you are sure that the computer will stop and say either ok or no. And if “no” you were the one who made the mistake.

6.4The product operation $`\mathrm{\Pi }`$: in the above expression, what is the type of `f`? We need a new operator $`\mathrm{\Pi }`$ written as `f:forall (x:A), B x` where

```
B:=fun (x:A) => "the type of (...x ... x ....) when x has type A"

```

(recall that the allowability restriction on `f` requires that this expression `(B x)` exist, and in fact it is calculable).

6.5Sorts: What is the type of a type? We are manipulating the types themselves as terms, so we are required to specify the type of a type. This is known as a “sort” (or in some literature, a “kind”). In current theories there are just a few, for example:
`Prop`, the type of propositions or statements; and
`Type_i`, the type of types which are thought of as sets (with a “universe index” `i`, see below), so an `X:Type_i` corresponds to a collection of objects, and an `x:X` corresponds to an element of the collection.

6.6Curry-Howard: In many (but not all) type-theory based systems, the notion of mathematical proof comes out for free from the type-checking algorithm. This is known as the “Curry-Howard principle”: propositions are realized as types, which the reader can think of as being sets with either zero or one element. Proving a proposition amounts to giving an element of the corresponding type, so the proof-checking mechanism is the same as the mechanism implementing the Church-Rosser algorithm refered to above, determining whether a given expression is indeed a term in the propositional type claimed by the mathematician. As suggested by the notation, the product operation $`\mathrm{\Pi }`$ corresponds to the logical “forall” in propositional calculus (a product of zero-or-one-element sets is nonempty if and only if all of the component sets are nonempty).

The above system corresponds to Martin-Löf’s type theory . One can imagine theories with a more complicated diagram of sorts, which is probably an interesting research topic for computer scientists.

6.7inductive objects: An interesting feature of a number of systems including `Coq` is the notion of inductive objects, which allows us automatically to create recursive datatypes. Since understanding and calculating with recursive datatypes is what the computer does best, it can be good to make use of this feature. It is often the only viable way of getting the computer hitched onto the calculational aspects of a problem. (This might change, notably with the advent of connectivity between theorem-proving systems and calculation systems.) We won’t go into any further detail on the basic structure or functionality of inductive definitions; the reader is referred to the reference manual of .

## 7. Universes

In order to get a coherent system (i.e. one without any known proofs of `False : Prop`) the sorts `Type_i` have to be distinguished by universe levels `i`, with `Type_i : Type_(i+1)` whereas `Type_i` $``$ `Type_(i+1)` also. In the set-theoretical semantics, these universe levels can be thought of as being Grothendieck universes, see . The incoherency of the declaration `Type:Type` without universe indices was shown in . Nonetheless, in some type-theoretical programs such as `Coq`, a vestige of `Type:Type` is preserved by a neat, but quirky, mechanism known as typical ambiguity (see ). The user just writes `Type` and the computer makes sure that it is possible to assign indices to all occurences of this word in such a way that the required inequalities hold. If this is not possible, then a `Universe Inconsistency` error is raised. Thus, the user writes his text file as if he were using the inconsistent `Type:Type` system, and the verification program then verifies that no unallowable advantage was taken.

Curiously enough, this leads to a phenomenon that looks for all the world to me like quantum mechanics.333This might be related to . Suppose you prove `A -> B` (i.e. “`A` implies `B`”) in one text file, and you separately prove `B -> C` in another. You might think you have proven `A -> C`. However, when you merge the two files together to get a proof of `A->C`, the verification program might come up with a `Universe Inconsistency` error if the constraints on the universe indices which are generated by the proofs of `A->B` and `B->C`, while separately satisfiable, are not satisfiable by any common assignment.

This phenomenon can be seen as a “disturbance due to measurement”. If we think of `A`, `B` and `C` as measuring posts along a lab bench (such as polarized glass panes, say `A` is horizontal, `B` is at $`45`$ degrees and `C` is vertical) then the result of starting with a photon polarized as `A`, doing the proof of `A-> B` and then “measuring” (i.e. stopping the text file and saying “wow, we just proved `B`”), then inputting the photon polarized as `B` into the next proof of `B -> C`, we get a photon polarized as `C` in the output; whereas if we do the whole proof starting from `A` and trying to get out `C`, no proof-photon comes through!

In  `qua.v`, a simple example of this phenomenon is given using Russell’s paradox, assuming the excluded middle and using `eqT_rect` via Maggesi’s proof of `JMeq_eq`  . As pointed out by H. Boom  it is possible (although more complicated) to do the same thing without axioms other than the basic `Coq` system, using the Burali-Forti paradox  .

It is important to note, then, that as long as the typical ambiguity mechanism is in place, it is not allowable to prove a theorem in one file and import it as an axiom in another file. It is actually required that the proofs of component pieces of the argument be imported by cut-and-paste (2.4). Luckily the system has a `Require` command that does this automatically without having to copy the files.

Questions about “universe polymorphism” lead to some of the most difficult notational problems. The following discussion comes from work of Marco Maggesi, who is also working on solutions to the problem possibly by implementing the thesis of Judicaël Courant . As was pointed out in , the basic example is the distinction between small categories and big categories, in other words assigning universe levels in the definition of category. Ideally, polymorphism should be extendable to definitions such as this. In the absence of such a mechanism, we seem to have to rewrite `Category_i` once for each level `i`. This can lead to a nightmare of notation, for example do we need to distinguish between a `comp_sm` for composition in a small category, and `comp_bg` for a big category? If this seems annoying but doable, notice that we then need `Functor_ij` for functors from a `Category_i` to a `Category_j`; and composing them, and so forth!

One of my main motivations for going back to a purely set-theoretic approach (cf 10.3, 10.4 below) is to try to avoid the above problems as much as possible. However, it seems that there will always be a threshold between the objects we are willing to manipulate and the bigger ones we would prefer not to manipulate, and looking at categories of the smaller objects inevitably bumps up against the bigger ones. Until someone comes up with an adequate general solution (perhaps the ideas in  are relevant) we are left with little choice but to live with the situation.

## 8. Exotic versus regular math

The system described above applies to a wide variety of situations, problems and logics.

8.1Intuitionism: One of the main utilizations of this type of system is to verify intuitionistic logic. In fact it is difficult to imagine taking a complicated argument and trying to insure, as a human reader, that the proof didn’t use the excluded middle in some hidden place in the middle. In this sense, computer verification seems crucially important and allows a much more serious approach to the field.

8.2Impredicative sort: in previous versions of `Coq` the sort `Set` was declared as impredicative,444In v8.0 the impredicativity is turned off and can apparently be turned back on by an option. in other words if `X:Set` then the product type

```
Set -> X := (Y:Set)X

```

is classified as having type `Set`. Nonetheless elements `X:Set` behave somewhat like sets: strong elimination is allowed, so that constructors in inductive sets are distinct. The intuition behind this situation is that the constructive functions on a constructive set themselves form a constructive set too. Thus these considerations are closely related to the constructive or algorithmic aspects of mathematics. Hugo Herbelin points out that this can lead to some unexpected and fascinating things, such as a proof which extracts to an algorithm where nobody can understand how it works .

8.3Caution: the existence of an impredicative but strongly eliminatory sort is somewhat “orthogonal” to standard mathematics, in that it contradicts most choice axioms you can imagine, even the much weaker dependent choice axioms  . Perhaps not all, though: David Nowak in  proposed doing the axiom of choice for the `Ensembles` library, which means looking at a function associating to any predicate `P:X->Prop` another predicate `(choice P):X->Prop` with the property that if `P` is nonempty then `(choice P)` is a singleton. One conjectures that this version is consistent even with an impredicative `Set`. Nowak’s version is difficult to use in practice, and leads to a situation where the only objects which are manipulated are predicates. This nullifies much of the advantage of using a type-theory framework. So, for implementing classical mathematics we prefer working without the impredicativity.

8.4Logic in a topos: recall from Moerdijk-MacLane  that one way of providing a model for certain intuitionistic logical systems is by looking at logic in a topos other than the topos of sets. One can say this differently (as they do in the book) by saying that any logical reasoning which is expressed solely in a limited intuitionist formulation, applies internally to logic within any topos. One can formulate as a conjecture, that this principle extends to the full intuitionist logical system as implemented in `Coq`:

ConjectureThe $`\lambda \mathrm{\Pi }`$ calculus with universes and inductive objects as described above and implemented in `Coq`, applies to logic within a Grothendieck topos.

It would be a generalization of the principles set out in . Some part of it may already be known, see Streicher  as well as the references therein (and indeed the formulation of the question appears to have been known to workers in Synthetic Domain Theory for some time  ). It is not immediate, for example, to see how to implement the sorts `Type_i`. A caveat might also be in order because recent versions of `Coq` include some inductive principles such as `False_rect` or `eqT_rect` which might not be realizable in the internal logic of a topos. So, the above statement is really just intended to point out that it is an interesting research problem to see how far we can extend the internal-logic principle from .

As an example of how this type of thing might actually lead to useful results for standard mathematics, one can use the full flexibility of the `Coq` implementation of type theory to define internal cohomology within the logic (this is done for $`H^1`$ in  `h1.v`). If this could be applied to a Grothendieck topos, it would show that cohomology in the topos was an internal logical construction. Internal algebraic geometry inside the topos of sheaves on the big fpqc site takes on a particularly nice form very close to the original Italian geometry, for example affine $`n`$-space is quite literally just the cartesian power of the ground field $`k^n`$.

8.5The Hodge conjecture: The statement of the Hodge conjecture implies that the problem of saying whether a given topological cycle is algebraic, is decidable. Same for the question of whether a given cycle is Hodge (i.e. vanishing of the Hodge integrals). This might be considered as a logical analogue of Deligne’s observation that the Hodge conjecture implies that Hodge cycles are absolute. The pertinance of calculatory methods showed up recently in . It could be interesting to investigate further, for example does Deligne’s proof of  imply the decidability for abelian varieties? And in exactly which level of intuitionist logic would the decidability hold? What are the consequences of this decidability given already by the Lefschetz $`(1,1)`$-theorem? What happens internally in a topos? Could one obtain a counterexample to the Hodge conjecture by showing that in some cases the question is undecideable?

——————–

8.6—So there are undoubtedly lots of fun things to look at in these exotic reaches, but they don’t really have anything to do with our original goal of implementing, as quickly as possible, a large amount of standard mathematics. More generally, my experience is that any “brilliant gadget” seems predestined to be a bad idea. Boring as it may seem, we have just to plod along in a mundane but systematic way.

## 9. Typed versus untyped style

One of the central questions in the theory has been whether to impose a strict type system, or whether to relax the typing constraints. There are some very interesting threads of discussion about the issue in the mailing lists, particularly  following the postings  and . It is interesting to note that in the first thread of discussion, Lamport (forwarded by Rudnicki ) offered the viewpoint that the untyped style was better than the typed one. He was promptly refuted by almost all the subsequent messages. A year later when Holmes  asked what options people generally used to answer the question, almost everybody replied that the untyped style was obviously the way to go. Unfortunately, this seems to have marked the end of interesting discussion on the QED mailing list . At about the same time the Coq system (where typed language was systematic) started picking up speed: the announcement of Coq Version 5.10 is among the last group of messages in Volume 3 of .

The published version of  is , issued from a combination of Lamport’s original note and a rebuttal by L. Paulson. This discussion and the discussion in J. Harrison  are excellent references for the multiple facets of the question which we don’t attempt further to reproduce here.

The distinction between the typed and the untyped style is generally seen as related to the axiom of choice. In the absence of the axiom of choice (in particular, in any sort of constructive environment) it is much more natural to keep a lot of type information, looking at the values of functions only when they are well defined and make sense. On the other hand, the axiom of choice provides a nice way to implement aspects characteristic of an untyped environment such as function evaluation which is defined everywhere .

Some authors make a distinction between choice and dependent choice, the latter stating only that we can choose a function whose values lie in a family of single-element types. By   this weaker form poses the same problems vis-a-vis a constructive axiom such as impredicativity of `Set`. Furthermore it generates a lot more proof obligations since one has to prove unicity whenever it is used. For this reason we don’t pay too much attention to the distinction, and look directly at the full axiom, even a strong Hilbertian form involving an $`ϵ`$-function.

## 10. Options for doing set theory

Sets are the most basic building blocks entering into the definition of various mathematical objects. On the other hand, as we have seen above, natural considerations about general mathematical theories lead to type theory as the framework for the system as a whole. The most critical decision about document style is therefore the way the notion of a set is encoded in the ambient type theory.

We will review some of the most prominent options. These follow the contours of the “typed versus untyped” discussion.

10.1Interpret sets as types. Benjamin Werner’s paper providing the justification for the $`\lambda \mathrm{\Pi }`$ calculus with inductive definitions  rests on a semantics, i.e. assignation of meaning to the formal symbols of the theory, where `X:Type_i` corresponds to a set in the $`i`$th Grothendieck universe $`U_i`$, and functions such as constructed by the $`\lambda `$ operation `fun x:A =>( ... x ... )` are represented by sets which are the graphs of the corresponding set-theoretic function. We can use this semantics as our method for interpreting sets, namely when we want to talk about a set we just take any `X:Type`. In this option we make full use of the notion of dependent types, see C. McBride . The following example shows how we would define the type of groups. It uses the `Record` construction which is a special inductive definition corresponding to an explicit list (of objects possibly depending on the previous ones).

```
Record Group : Type_(i+1) := {
elt:Type_i;
op : elt -> elt -> elt;
id : elt;
inv : elt -> elt;
assoc : forall x y z:elt,(op (op x y) z) = (op x (op y z));
left_id : forall x:elt, (op id x) = x;
right_id : forall x:elt, (op x id) = x;
left_inv : forall x:elt, (op (inv x) x) = id;
right_inv : forall x:elt, (op x (inv x)) = id
}.

```

With this definition, if `G:Group` then `(elt G):Type_i` is the “set” of elements of `G`.

The advantage of this viewpoint is that it is generally quite easy to understand what is going on. You the uninitiated reader didn’t have any trouble reading the previous definition, and could by cut and paste give the analogous definition of, say, `Ring`, right?

One of the drawbacks with this point of view is that if `H:Group` too, and if for some reason we know `G=H`, we have problems interpreting elements of `G` as being the same as elements of `H`. For example it is not legal to write

```
forall x y z:(elt G), (op H (op H x y) z) = (op G x (op G y z))

```

(if rare at the outset, this sort of thing tends to come up in the middle of proofs). The problem is alleviated by the recent inclusion in `Coq` of the “transport” function `eqT_rect`, the utilisation of which is best accompanied by a systematic exploitation of the `JMeq` equality proposed by McBride . This doesn’t make the problem go away entirely, though.

This point of view adheres pretty closely to the “typed” side of the discussion in the previous section. An appropriate choice axiom could allow us to extend function definitions to larger types, whenever a default is available. Unfortunately this implies a distinction between empty and nonempty types. Some have made more exotic proposals to include a default element $``$ in every type (this is based on work of Scott , and was mentionned in the replies to ). I haven’t looked closely at it, mostly for fear of a large number of proof obligations of the form $`x`$, and because it obviates the advantage that we can easily understand what is going on. Also because the guy in the office next door talks about it so much.

To close this subsection we also mention another more subtle drawback, which might really be the main problem. There is a very slight shift in universe indexing, compared with what we are used to in set theory. In the above `Record` if we want the underlying set `(elt g)` to be in the universe `Type_i`, the type `Group` is forced to be in the universe `Type_(i+1)`. In general, a set at a given universe level will also have elements at that level. Thus, a priori, the elements `g:Group` are to be considered (even though this statement doesn’t have any precise technical meaning) as being in the $`(i+1)`$-st level. This contrasts with set theory where, if `g` is a group whose underlying set `(elt g)` is in the $`i`$-th universe, then `g` is represented by an ordered uple which is also in the $`i`$-th universe.

10.2Setoids. From a constructive point of view, the notion of a quotient can be problematic because an equivalence relation need not be decidable, so when defining an object as a carrier modulo a relation, the carrier might be constructive or computational but the quotient less so. Another problem is that the classical construction of a quotient as a set of equivalence classes can pose problems in certain intuitionist frameworks (imagine doing that internally in a topos, for example).

For these (or perhaps other) reasons a much-favored implementation of sets is as setoids (cf the `Setoid` libraries in `Coq`). A setoid is a carrier type together with an equivalence relation. We can think of them as quotient sets without adding additional axioms. One major drawback is that there is a lot of extra stuff to prove, basically that all operations defined on the level of the carrier type are compatible with the equivalence relation.

For standard mathematics, we don’t really need the setoid viewpoint since we are willing to add in all of the axiomatic baggage which makes the usual theory of quotients go through. What is useful is to know that such structures exist, are natural, and have been studied, because they occasionally show up uninvited.

10.3Introduce a type `E` of sets. In this viewpoint, the type-level is considered as the meta-language of mathematical expressions, and we introduce maybe some parameters

```
Parameter E : Type.
Parameter inc : E -> E -> Prop.

```

Here `E` is for “Ensemble” and `inc` is the elementhood relation. One can then go on to suppose all of the usual axioms in set theory, and proceed from there. For example the definition of the subset relation becomes

```
Definition sub := [a,b:E](c:E)(inc c a) -> (inc c b).

```

A development of set theory using this type of viewpoint was done by Guillaume Alexandre in his Coq contribution “An axiomatisation of intuitionistic Zermelo-Fraenkel set theory” (1995) . This version is also quite analogous to the foundations of the MIZAR system , and has been developped rather deeply in the “ZF” logic in the Isabelle system .

One can even create such an `E` using an inductive definition and a quotient, see Aczel  and Werner :

```
Inductive Ens : Type := sup : (A:Type)(A->Ens)->Ens.

```

This is a carrier type, bigger than what we actually think of as $`Ens`$ because an equivalence relation of extensional equality is defined (thus, `E` should actually be thought of as a setoid and to get a type we would have to take the quotient). Once we have the basic axioms, which in these constructions may require supposing their counterpart axioms on the type-theory side , the further development of the theory doesn’t require knowing about the construction, so in this sense it is conceptually easier just to take `E` as a parameter.

In theories of this option, sets are terms of type `E`, but not themselves types, and elementhood is just a propositional relation on `E`. This is contrasted with the type-theoretical interpretation (10.1) where the relation `x:X` is meta to the theory, not actually accessible from within, and is decided by the computer.

This would seem at first glance to be much less powerful than version (10.1) where sets are types. In a certain sense that’s true, but in some other ways it is actually more powerful. The fact that the elementhood relation is a propositional function in the theory allows us to manipulate it mathematically. The problem referred to above about elements of sets which are equal, goes away: if `a=b` and if `x:E` then the propositions `(inc x a)` and `(inc x b)` are equal since they are functions of `a=b`. Inside proofs, the fact that a certain term has a certain type is replaced by the statement that a certain set is an element of another set; in the first case the knowledge is required at the start because otherwise the statement will be rejected by the type-checker, but in the second case the proof can be deferred into a separate branch of the proof tree.

If we further add an appropriately strong version of the axiom of choice (basically Hilbert’s $`ϵ`$) then we get an even better situation   where function evaluation can be defined as the operation which to any `f,x:E` assigns a choice of `y:E` such that the pair `(pair x y)` is contained in `f`, if such a `y` exists (or a default value if no such exists). In fact, if we write down all of the axioms in this general spirit of everywhere-definedness, then everything that follows will be everywhere-defined too, and we are no longer bothered with objects depending on proofs of propositions.

The main disadvantage of the purely set-theoretical approach is that we have lost any possibility for the computer directly to compute on sets, because computation requires specific knowledge about the inductive structure of the type containing a given term and our `E` no longer has any inductive structure. (This might well be alleviated using the direct constructions of  and , though, a thought-experiment that starts off the next option.)

10.4Combine 10.1 and 10.3. In the Aczel-Werner type constructions  one can construct a set i.e. term `x:E` whenever one has a type `A:Type` together with a realization function for its elements `A -> E`. Imagine that we want to realize as a set an inductive type say

```
Inductive nat : Type :=  O : nat | S : nat -> nat.

```

To do this we would need to construct an injection `nat -> E`. In this particular case it is natural to do so because the construction

$$\mathrm{},\{\mathrm{}\},\{\mathrm{},\{\mathrm{}\}\},\mathrm{}$$

played an important historical role in the beginning. However, if we try to do the same for, say, a free monoid, few people ever really worry about the details of how to do it. This requirement would therefore seem to qualify as something that doesn’t have any real mathematical significance: we only care about the universal properties of an inductive type, not about how it is actually realized.

In Werner’s paper , he describes briefly how to realize inductive types as sets, and consequently how to realize every type as a set. So, let’s just abstract out this process and suppose, with a parameter, that we know how to do it but we don’t care what it is. We get a situation where, combining (10.1) and (10.3), sets are types, but also the elements of sets are realized as sets themselves—which after all is the bedrock assumption of classical set theory.

This is the viewpoint which is developped in . We start by putting

```
Definition E:= Type.
Parameter R : (x:E)x->E.
Definition inc := [a,x:E](exists [b:x](R b) = a).

```

Thus, we identify the notion of set with the notion of type. The parameter `R` is the realization function which says that the elements of a set/type are themselves sets. The elementhood relation `inc` is defined using `R` by saying that $`ax`$ iff there exists a term $`b`$ of type $`x`$ whose realization is $`a`$.

We assume a certain number of axioms such as choice (in the form of a Hilber $`ϵ`$-function) and replacement. We can then go on to develop set theory for `E` just as would be done in option (10.3) above. On the other hand, we can calculate with inductive types and other type-theory features, useful among other things to establish a notational system.

## 11. Inheritance

Consider the notion of Lie group. This fits into at least 4 distinct (plus one overlapping) inheritance threads as shown in Figure 1.

The three rightmost threads are formally similar, however the ringed spaces in question are different, and the topological spaces for the two middle threads are the same but different from the (Zariski) topological space in the “algebraic variety” thread. One could identify other inheritance strings, and note that there are intricate relationships between them, for example the structure sheaf of the ringed space underlying the complex variety is a subsheaf of the structure sheaf of the ringed space underlying the differentiable manifold, and the set underlying the usual topological space in the first threads is the subset of closed points in the set underlying the Zariski topological space.

If $`G`$ is a Lie group, informally we tend to use the letter “G” for any and all of the above things and more.

On the other hand, the details of these inheritance relations would have precisely to be spelled out in any computer verification system.

Letting the same letter “G” mean any of an amorphous mass of notions, represents a huge collection of notational shortcuts. While clearly impossible to keep all of them, it should be possible to keep some. This could lead to some difficult choices: how to decide which parts to keep and which parts to relegate to a more complicated notation. And in any case, how do we minimize the amount of additional notation necessary to make these shortcuts precise?

The example of a Lie group is deliberately complex in order to illustrate the problem. However, it comes up to varying degrees in pretty much all of modern mathematical practice.

## 12. Perspectives

We now outline a sketch of what some part of the further development of machine-verified mathematics might look like. This could start with any of a number of basic supports such as , , , , …, some of which are already quite far along.

Attached to the original preprint version of the present paper was the start of a development along the lines of option (10.4) above. The idea of notative sets as being functions on strings, first brought up in , was implemented. We get a primitive kind of inheritance, in which different structures corresponding to different strings can coexist in the same object, and the functions extracting these operations from a given object are uniform throughout. Thus for example the theory of groups and the theory of topological spaces would both apply immediately to topological groups. The explanatory section and source code have now been spun off as a separate preprint .

The proof development accompanying  now treats the notions of ordinal and cardinal. The next part which needs to be addressed would contain the notion of finiteness, various facts about finite sets (notably that any automorphism of a finite set decomposes as a product of transpositions); also various notions of collection or list of objects; etc. The theory of transpositions should help for defining multi-term summation in an abelian monoid.

Most objects are constructed with a single common variable, denoted `(U a)`, thought of as the “underlying set” of `a`. Morphisms between such objects can be considered as some of the maps between underlying sets. This makes it possible to develop a certain amount of categorical machinery at once for all these types of objects.

With this in mind, we can define monoids, groups, rings, algebras, modules; categories, eventually with Grothendieck topologies; presheaves (and sheaves if the category has a g.t.); ordered sets; topological spaces also eventually with other structures so that one could define topological groups and so on.

The counting system has to be extended to the numbering system. We can import much of the beautiful development of Peano arithmetic already in the `Coq` system, as well as the `ZArith` library containing a logarithmically fast implementation of integers. Then we need to define the rationals as a localization of the integers (and for this we might as well call upon the general notion of localization of a ring). Then we can define the reals as the set of Dedekind cuts of the rationals. It is not clear whether it is better to import the real number results from the existing `Coq` library, or to redo a substantial portion, since our approach using things like the axiom of choice, and an untyped point of view, might give substantial simplification here (as opposed to the case of elementary arithmetic where we wouldn’t expect any such benefit).

Once we have the reals (and therefore the complex numbers too) we need to establish the basic facts about the topology on these spaces, and along the way note that this opens up the definition of metric space, so we can do the basic facts about metric spaces. This could eventually lead to stuff for analysis such as Hilbert or Banach spaces, and all of the basic theorems of analysis. This is not necessarily urgent although it would be required for the implementation of Hodge theory.

A parallel project is to develop abstract commutative and linear algebra as well as group theory and field theory. For large parts, these theories don’t need the real numbers. As pointed out above, the notion of localization would be convenient to have for the construction of the rational numbers. In general, it would be good to start by developing the basic commutative algebra such as is assumed in the beginning of Hartshorne. Once we have a reasonable control over the basic notions of ring, algebra, module etc. then much of commutative algebra can be done without any new notational worries.

Linear algebra could lead to a rather extensive development of the theory of matrices, matrix groups, and group representations.

Again in parallel, we need the notions of presheaf and sheaf over a topological space. Here it seems economical to take the abstract point of view and develop directly the notion of sheaf on a Grothendieck site. Along the way the notion of presheaf on a category yields the notion of simplicial set which forms the basis for homotopy theory. The notion which is directly useful for starting out is that of sheaf on a topological space, so we need a construction going between a space and its corresponding Grothendieck site of open sets. It is unclear whether we would prefer using the full abstract notion of point for a site (or maybe a topos?—but this may lead to universe problems) or whether it is better just to look at the germ for a presheaf on a topological space. In any case, here some ad hoc argumentation is necessary, because we would like the germ of a presheaf to be endowed with the same type of structure as the presheaf; the variety of different types of structures we want to preserve means that it is probably more difficult to come up with a single general theory than just to do each one separately.

Up to here, most of what is listed above has already been treated in one way or another, in at least some user-contributions for at least some of the systems listed in the bibliography. Left open is the problem of coalescing everything together.

Once we have these various theories, we can put them together to obtain the notion of locally ringed space modelled on a certain type of model space. Depending on which model spaces we look at, we can obtain the notions of differentiable manifold, complex analytic manifold, or algebraic variety (scheme). Laurent Chicli has done a formalization up to the notion of (affine) scheme in his thesis , using setoids (option (10.2) above).

At this point, perhaps one of the first things to do would be the comparison constructions going from schemes (over $`𝐂`$) to complex manifolds to differentiable manifolds. We should then be able to construct projective space, projective subvarieties, various differentiable manifolds, and so on. Another thing to do will be exterior algebra and differential calculus over a manifold.

It would be interesting to try things out by applying this to the case of Lie groups, and seeing how far into the theory one can go.

Integration is probably the next place where we will run into a major notational problem. This is because the verb “to integrate” spans a highly diverse and notationally wide-ranging collection of ideas: there is simple Riemann (or Lebesgue) integration on the real line (already implemented in ), but also more general integration of a measure, or integration of a differential form over various things such as a manifold, or a smooth chain; or finally integration of currents and the like. These different notions have a very high degree of overlap, however they are not quite the same, and they require differing notations and even differing levels of notational complexity.

With the theory of integration would come the possibility of getting at the fundamental properties of analysis on manifolds. At this point we will need the theory of Hilbert and Banach spaces (already implemented in ), and we should be able to do the basic theorems such as Stokes’ theorem, the Poincaré lemma and de Rham’s theorem, Hartogs’ theorem for complex manifolds, the mean value theorem for harmonic functions, which gives the maximum principle and unicity of analytic continuation, the representation (and regularity) of cohomology by harmonic forms, leading up to the Hodge decomposition for the cohomology of a complex Kähler manifold (to take an example from my own research interests). At this stage we will also want to have the basic notions of homotopy theory available.

Once all of the above is well in hand, we would be able to state and prove a first theorem which is a really nontrivial application of this wide swath of mathematics: the fact that the first (or any odd) Betti numbers of complex algebraic varieties are even.

We should then be able to start looking at more advanced things going toward current research problems. One area where we can expect important gains is homological or homotopical algebra, for example J. Lipman points out that it would be good to formalize the computations in duality theory such as . More geometrical directions could include for example the construction of moduli spaces of vector bundles, connexions and so forth. Or the investigation of existence problems for connexions over higher dimensional varieties which could at first be viewed just as matrix problems in linear algebra.

Some day in the not-too-distant future we will have a computer-verified proof that the curvature of the classifying space for variations of Hodge structure in the horizontal directions is negative, and all that it entails.


format: text

text:
# Bernoulli potential in type-I and weak type-II superconductors: Surface charge

## I Historical review

The electrostatic potential in superconductors is known already for seven decades. Within the pre-London approaches based on the ideal charged liquid, the electrostatic potential was assumed to balance the Lorentz and the inertial forces acting on diamagnetic currents. The current $`𝐣=en𝐯`$ flows along the surface and its amplitude falls off exponentially from the surface into the bulk. Similarly the screened magnetic field decays. The balancing electrostatic potential was found to be of the Bernoulli type, $`e\phi =\frac{1}{2}mv^2`$, therefore it falls off on the scale of half the London penetration depth. From the Poisson equation,

$$ϵ_0^2\phi =\rho ,$$
(1)
one finds that this corresponds to a charge accumulated in the layer penetrated by the magnetic field. To maintain the charge neutrality, the accumulated bulk charge has to be accompanied by the opposite surface charge. This picture has been confirmed by the London theory.

### A Advanced London-type approaches

The electrostatic potential equals the Bernoulli potential only at zero temperature when all electrons are in the superconducting condensate. At finite temperatures, a part $`n_n`$ of electrons remains in the normal state, while the rest $`n_s=nn_n`$ contributes to the supercurrent, $`𝐣=en_s𝐯`$. The electric force acting on normal electrons is transferred to the condensate via a mechanism which reminds one of the fountain effect in superfluid helium. As a consequence, the electrostatic potential reduces to $`e\phi =\frac{n_s}{n}\frac{1}{2}mv^2`$. This reduction of the potential derived by van Vijfeijken and Staas has a somehow confusing name: the quasiparticle screening. It should be noted that the electrostatic potential caused by currents in superconductors is traditionally called the Bernoulli potential in spite of the quasiparticle screening and other non-Bernoulli contributions found later.

Jakeman and Pike recovered the result of van Vijfeijken and Staas from the static and the classical limit of the time-dependent Ginzburg-Landau (GL) theory. Unlike previous studies, their approach includes the real screening due to spatial distribution of the charge, therefore it describes the surface charge as a space charge localized on the scale of the Thomas-Fermi screening length. This picture of the surface charge was accepted for a long time as it looks natural and seems to be justified from the semi-microscopic theory.

Later studies of the electrostatic potential did not re-address the question of the surface charge but attempted to overcome the hydrodynamic picture common to all the above mentioned studies. Naturally, they focused on a detailed description of the Bernoulli potential on the scale of the London penetration depth.

Adkins and Waldram recovered the Bernoulli potential from the BCS theory for the system at zero temperature. They also indicated that at finite temperatures one should expect a contribution which depends on the band structure.

The predicted contribution has been evaluated by Rickayzen. He used the thermodynamic approach which yields

$`e\phi ={\displaystyle \frac{n_s}{n}}{\displaystyle \frac{1}{2}}mv^2.`$ (2)
The density dependence of the condensate density can be evaluated either from the BCS theory leading to the result of Adkins and Waldram or from the two-fluid relation $`n_sn\left(1\frac{T^4}{T_c^4}\right)`$. The latter gives a simple formula

$`e\phi ={\displaystyle \frac{n_s}{n}}{\displaystyle \frac{1}{2}}mv^24{\displaystyle \frac{n_n}{n}}{\displaystyle \frac{\mathrm{ln}T_c}{\mathrm{ln}n}}{\displaystyle \frac{1}{2}}mv^2.`$ (3)
The first term balances the Lorentz and inertial forces, while the second reflects the pairing. We will call terms proportional to $`\frac{\mathrm{ln}T_c}{\mathrm{ln}n}`$ the thermodynamic correction.

In the next decade, the interest in the electrostatic potential in superconductors shifted towards non-equilibrium situations, see e.g. Ref. . It should be noted that the Bernoulli potential introduced within the theory of non-equilibrium systems is not the same as the one we discuss. Within the non-equilibrium theory the term Bernoulli potential is used for the velocity-dependent part of the energy of Cooper pairs. Only in equilibrium, the velocity-dependent energy agrees with the electrostatic potential we discuss here.

### B GL approaches – local

New studies of the Bernoulli potential in equilibrium have been stimulated by the question of the vortex charge. Khomskii et al. have used the idea of van der Marel to derive a simple estimate of the electrostatic potential in terms of the superconducting gap. The obtained formula corresponds to the thermodynamic correction of Rickayzen with the original balance term being omitted. While the validity of the approach is restricted to temperatures close to $`T_c`$, it has the advantage, however, that it can be applied within the GL theory. Blatter et al. have employed this estimate to predict a possible electrostatic field above the surface of the superconductor with the vortex lattice perpendicular to it.

An opposite limit represents the treatment of the vortex charge by LeBlanc. He considers only the balance term omitting the thermodynamic correction completely. As one can see from Rickayzen’s formula, this approximation is limited to the region of low temperatures.

### C GL approaches – non-local

All the above mentioned theories have in common that the electrostatic potential is a local function of the classical kinetic energy or of the gap. In other words, they neglect the gradient of the condensate. The non-local corrections within the GL theory have been proposed in Ref. . It turned out that the non-local corrections are taken into account if the classical kinetic energy in the balance equation is replaced by its quantum-mechanical counterpart.

For our next discussion it is important that the non-local contributions can be rearranged into a local form. Indeed, within the GL theory the sum of the kinetic energy and the GL potential is zero which allows us to express the balance term via the local GL potential. Note that this rearrangement is possible only within the non-local theory, because gradients of the condensate density $`n_s=2|\psi |^2`$, where $`\psi `$ is the GL wave function, provide important contributions to the quantum kinetic energy, in particular close to the surface.

In Ref. , the quasiparticle screening and the thermodynamic correction have been neglected, the complete theory has been presented in Ref. . The detailed derivation together with estimates of material parameters and the numerical treatment of the Abrikosov vortex lattice in niobium at various temperatures can be found in Ref. . Again, all contributions including the kinetic energy can be expressed in a local relation $`\phi [|\psi |^2]`$.

The non-local form of the Bernoulli potential requires to reconsider the picture of surface charges. It is paradoxical that the possibility to rearrange the non-local corrections into a local function plays the crucial role. As noticed already by Yampolskii et al., if the electrostatic potential is of the form $`\phi [|\psi |^2]`$, the GL boundary condition, $`\psi =0`$ in the direction normal to the surface, implies that no surface charge is needed. Indeed, at the surface $`\phi =\frac{\phi }{\psi }\psi =0`$. The electric field thus vanishes at the surface which is a sufficient condition for the charge neutrality.

### D Plan of the paper

Apparently, there is no surface charge on the scale of the Thomas-Fermi screening length. The electric field due to the dipole between the surface charge and the bulk charge was supposed to balance the Lorentz force, therefore one has to ask the question how the balance of forces looks if the surface charge is absent.

The charge profile in the vicinity of the surface has been numerically studied in Ref. . This study was limited to thin slabs and type-II superconductors, its results indicate, however, that the charge profile at the surface tends to organize into two layers - a narrow surface charge and a thicker bulk charge.

In this paper we discuss the charge and potential profile at the surface of a semi-infinite superconductor in the Meissner state. In the next section we shortly describe the surface charge within the GL theory. In section III we discuss the limit of a weak magnetic field, where all results can be derived analytically. We will show that the Bernoulli potential at the surface differs from the value predicted by Rickayzen. The correction has the form of a multiplicative factor that approaches unity for the extreme type-II superconductor. Numerical results on strong magnetic fields are presented in section IV revealing a nonlinear mechanism which, however, is found to be very small. The conclusions and outlook are presented in section V.

## II Surface charge within the Ginzburg-Landau type theory

A typical profile with the charge distribution close to the planar surface and homogeneous external magnetic fields is shown in Fig. 1. The profile has been obtained by a numerical solution of the GL equation

$$\frac{\mathrm{}^2^2}{2m^{}}\psi +\frac{e^2𝐀^2}{2m^{}}\psi \frac{\gamma T_c^2}{2n}\left(1\frac{t^2}{\sqrt{1\frac{2}{n}\psi ^2}}\right)\psi =0,$$
(4)
where $`n`$ is the density of pairable electrons, $`\gamma `$ is the linear coefficient of the specific heat, $`m^{}=2m`$ and $`e^{}=2e`$ are the mass and charge of the Cooper pair, and $`t=T/T_c`$ is the temperature on the scale of the critical temperature. In the assumed geometry one can use the London gauge in which the GL wave function is real.

Equation (4) has been proposed by Bardeen as an extension to low temperatures. In fact, Bardeen arrived to this equation independently adding the quantum kinetic energy to the Gorter-Casimir two-fluid model. Close to the critical temperature the GL function has a small magnitude $`2\psi ^2n`$ which allows one to expand the square-root $`1/\sqrt{1\frac{2}{n}\psi ^2}1+\frac{1}{n}\psi ^2`$, and one finds the customary GL equation with parameters $`\alpha =\gamma T_c^2(t^21)/2n`$ and $`\beta =\gamma T_c^2t^2/n^2`$.

The vector potential $`𝐀`$ is given by the Maxwell equation

$$\times \times 𝐀=\mu _0\frac{e^2}{m^{}}\psi ^2𝐀.$$
(5)
Equations (4) and (5) are solved together with $`\gamma `$ and $`T_c`$ kept constant.

From the GL wave function $`\psi `$ we evaluate the Bernoulli potential

$`e\phi \lambda _{\mathrm{TF}}^2^2e\phi `$ $`=`$ $`{\displaystyle \frac{\gamma T_c^2}{2n^2}}\left(1{\displaystyle \frac{t^2}{\sqrt{1\frac{2}{n}\psi ^2}}}\right)\psi ^2`$ (7)
$`+{\displaystyle \frac{\psi ^2}{2n}}{\displaystyle \frac{\gamma T_c^2}{n}}+{\displaystyle \frac{t^2T_c^2}{2}}{\displaystyle \frac{\gamma }{n}}\sqrt{1{\displaystyle \frac{2}{n}}\psi ^2}.`$
The density dependence of $`\gamma `$ and $`T_c`$ has been estimated from the experimental specific heat, theoretical free-electron density of states, and the McMillan formula, see Appendix in Ref. . The Thomas-Fermi screening length, $`\lambda _{\mathrm{TF}}^2=\frac{\pi ^2k_B^2ϵ_0}{\gamma e^2}`$, is very small and its contribution can be neglected, because the general integral which is proportional to $`\mathrm{exp}(x/\lambda _{\mathrm{TF}})`$ is zero since no surface charge forms on this scale.

In the final step the charge profile is evaluated from the Poisson equation (1).

## III Low magnetic fields

In weak magnetic fields the GL wave function is only little perturbed from its bulk value $`\psi =\psi _{\mathrm{}}+\delta \psi `$ with $`\delta \psi \psi _{\mathrm{}}`$. In this limit the charge profile can be solved analytically.

In the Maxwell equation (5) the vector potential is a small quantity so that the perturbation of the wave does not contribute in lowest order. The vector potential can thus be solved taking $`\psi \psi _{\mathrm{}}=\sqrt{n(1t^4)/2}`$. For both types of superconductors, this results in a simple exponential decay of the vector potential,

$$A_xB\lambda \mathrm{e}^{x/\lambda }.$$
(8)
on the scale of the London penetration depth $`\lambda =\lambda _0/\sqrt{1t^4}`$, with $`\lambda _0^2=2m^{}/(\mu _0e^2n)`$. Here $`B`$ is the value of the magnetic field at the surface at $`x=0`$.

### A GL wave function

The linear approximation of the GL equation (4) reads

$$\frac{\mathrm{}^2^2}{2m^{}}\delta \psi \frac{\gamma T_c^2t^2}{n^2}\left(1\frac{2}{n}\psi _{\mathrm{}}^2\right)^{\frac{3}{2}}\psi _{\mathrm{}}^2\delta \psi =\frac{e^2𝐀^2}{2m^{}}\psi _{\mathrm{}},$$
(9)
which can be expressed in terms of the GL coherence length $`\xi ^2=2\mathrm{}^2nt^4/(m^{}\gamma T_c^2(1t^4))`$ as

$$^2\delta \psi \frac{2}{\xi ^2}\delta \psi =\frac{e^2}{\mathrm{}^2}\psi _{\mathrm{}}\lambda ^2B^2\mathrm{e}^{2x/\lambda }.$$
(10)
The solution of (10) is composed from the particular integral with the decay on the scale of the London penetration depth and the general integral decaying on the scale of the GL coherence length,

$$\delta \psi =\psi _\lambda \mathrm{e}^{2x/\lambda }+\psi _\xi \mathrm{e}^{\sqrt{2}x/\xi }.$$
(11)
The general integral of (10) can also include a growing term $`\mathrm{exp}(\sqrt{2}x/\xi )`$. This term is excluded, because the perturbation asymptotically vanishes in the bulk, $`\delta \psi 0`$ for $`x\mathrm{}`$.

From the GL boundary condition, $`\delta \psi =0`$ at $`x=0`$, we find that the two amplitudes are linked by

$$\psi _\xi =\frac{\sqrt{2}}{\kappa }\psi _\lambda ,$$
(12)
where $`\kappa =\lambda /\xi `$. We note that within Bardeen’s extension of the GL theory, the ratio $`\lambda /\xi `$ depends on the temperature, $`\kappa =\kappa _{\mathrm{GL}}/t^2`$, where $`\kappa _{\mathrm{GL}}=\frac{m^{}T_c}{ne^{}\mathrm{}}\sqrt{\frac{\gamma }{\mu _0}}`$ is the ordinary GL parameter defined at $`T_c`$. The diverging effective GL parameter at low temperatures shows that within Bardeen’s approximation any system behaves as a type-II superconductor at sufficiently low temperatures. This feature contrasts with the linearly decreasing effective GL parameter one finds close to the upper critical magnetic field.. Of course, the strong temperature dependence of $`\kappa `$ is rather an artifact of the model. Since $`\kappa `$ is the most important quantity of the GL theory, one can simply take $`\lambda `$ and $`\kappa `$ as input parameters.

The amplitude of the particular integral is obtained from the GL equation (10) as

$$\psi _\lambda =\psi _{\mathrm{}}\frac{\frac{e^2}{\mathrm{}^2}\lambda ^2B^2}{\frac{4}{\lambda ^2}\frac{2}{\xi ^2}}=\psi _{\mathrm{}}\frac{e^2\lambda ^4B^2}{2\mathrm{}^2}\frac{1}{2\kappa ^2}.$$
(13)
The GL wave function from (11-13) results in

$$\delta \psi =\frac{\psi _{\mathrm{}}}{2\kappa ^2}\frac{e^2\lambda ^4B^2}{2\mathrm{}^2}\left(\mathrm{e}^{2x/\lambda }\frac{\sqrt{2}}{\kappa }\mathrm{e}^{\sqrt{2}x/\xi }\right).$$
(14)
### B Bernoulli potential

Finally, we take the linear approximation of the Bernoulli potential (7) in $`\delta \psi `$. Since the asymptotic value of the potential $`\phi _{\mathrm{}}=\phi [|\psi _{\mathrm{}}|^2]`$ is not essential, we focus on the perturbation caused by the magnetic field

$$e\delta \phi \lambda _{\mathrm{TF}}^2^2e\delta \phi =C\delta \psi .$$
(15)
In terms of $`\lambda `$ and $`\kappa `$ the coefficient $`C`$ reads

$$C=\frac{\mathrm{}^2\kappa ^2}{2m^{}\lambda ^2\psi _{\mathrm{}}}\left(1t^4+4t^4\frac{\mathrm{ln}T_c}{\mathrm{ln}n}\right).$$
(16)
A general integral which decays into the bulk is of the form

$$e\delta \phi =e\delta \phi _{\mathrm{TF}}\mathrm{e}^{x/\lambda _{\mathrm{TF}}}+C_\lambda \psi _\lambda \mathrm{e}^{2x/\lambda }+C_\xi \psi _\xi \mathrm{e}^{\sqrt{2}x/\xi }.$$
(17)
From (15) one finds the amplitudes

$`C_\lambda `$ $`=`$ $`{\displaystyle \frac{C}{14\frac{\lambda _{\mathrm{TF}}^2}{\lambda ^2}}},`$ (18)
$`C_\xi `$ $`=`$ $`{\displaystyle \frac{C}{12\frac{\lambda _{\mathrm{TF}}^2}{\xi ^2}}}.`$ (19)
The amplitude of the general integral is given by the charge neutrality, which requires $`\delta \phi =0`$ at $`x=0`$. From (17) follows

$$e\delta \phi _{\mathrm{TF}}=2\frac{\lambda _{\mathrm{TF}}}{\lambda }C_\lambda \psi _\lambda \sqrt{2}\frac{\lambda _{\mathrm{TF}}}{\xi }C_\xi \psi _\xi .$$
(20)
The relative amplitudes proportional to $`\lambda _{\mathrm{TF}}/\lambda `$ and $`\lambda _{\mathrm{TF}}/\xi `$ are not sufficiently small to be neglected. The charge density is given by the second derivatives so that one obtains relative amplitudes of the charge density at the surface proportional to $`\lambda /\lambda _{\mathrm{TF}}`$ or to $`\xi /\lambda _{\mathrm{TF}}`$. The surface charge is an integral, i.e. the contribution in question is proportional to the amplitude at the surface multiplied with the Thomas-Fermi length. According to condition (20) all charges can have comparable values.

To prove that the screening on the scale of the Thomas-Fermi length $`\lambda _{\mathrm{TF}}`$ and the related surface charge can be neglected, one has to employ the GL boundary condition $`\delta \psi =0`$ at $`x=0`$. Using (12) one obtains

$$e\delta \phi _{\mathrm{TF}}=\frac{\lambda _{\mathrm{TF}}^3}{\lambda ^3}\frac{4(2\kappa ^2)}{12\kappa ^2\lambda _{\mathrm{TF}}^2/\lambda ^2}C_\lambda \psi _\lambda $$
(21)
so that the general integral is proportional to the cube of the small ratio $`\lambda _{\mathrm{TF}}/\lambda `$. Accordingly, the charge due to the general integral is smaller by a factor $`\lambda _{\mathrm{TF}}^2/\lambda ^2`$ than the charge created by the particular integral. In the following we neglect this contribution for simplicity of notation. Within the same level of accuracy we take $`C_\lambda =C`$ and $`C_\xi =C`$.

Now we are ready to evaluate the electrostatic potential. Using (12) and (13) we obtain from (17)

$`e\delta \phi `$ $`=`$ $`{\displaystyle \frac{B^2}{2\mu _0n}}\left(1+{\displaystyle \frac{4t^4}{1t^4}}{\displaystyle \frac{\mathrm{ln}T_c}{\mathrm{ln}n}}\right)`$ (23)
$`\times {\displaystyle \frac{1}{1\frac{2}{\kappa ^2}}}\left(\mathrm{e}^{2x/\lambda }{\displaystyle \frac{\sqrt{2}}{\kappa }}\mathrm{e}^{\sqrt{2}x/\xi }\right).`$
This linearized relation extends Rickayzen’s formula to type-I and weak type-II superconductors.

Let us first take a look at the extreme type-II superconductor, $`\kappa 1`$, for which Rickayzen’s formula is recovered. For the assumed real GL wave function, the current is proportional to the vector potential $`𝐣=\frac{e^2}{m^{}}\psi _{\mathrm{}}^2𝐀=\frac{e^2}{m}n_s𝐀`$. With the velocity defined via the current, $`𝐣=e^{}\psi _{\mathrm{}}^2𝐯=en_s𝐯`$, one finds from (8) the relation between the magnetic pressure and the kinetic energy $`\mathrm{e}^{2x/\lambda }\frac{B^2}{2\mu _0n}=\frac{n_s}{n}\frac{1}{2}mv^2`$. Equation (23) yields then the Bernoulli potential as

$`e\delta \phi `$ $`=`$ $`{\displaystyle \frac{1}{2}}mv^2\left({\displaystyle \frac{n_s}{n}}+4{\displaystyle \frac{n_n}{n}}{\displaystyle \frac{\mathrm{ln}T_c}{\mathrm{ln}n}}\right)`$ (25)
$`\times {\displaystyle \frac{1}{1+\frac{\sqrt{2}}{\kappa }}}\left(1+{\displaystyle \frac{\mathrm{e}^{\left(1\kappa /\sqrt{2}\right)2x/\lambda }1}{1\frac{\kappa }{\sqrt{2}}}}\right).`$
We have used $`n_s=n(1t^4)`$ and $`n_n=nt^4`$ to express the temperature dependence in terms of the condensate fraction.

One can see that Rickayzen’s formula (3) holds for extreme type-II superconductors, $`\kappa \mathrm{}`$. In this limit the general integral has a vanishingly small amplitude and the factor $`1/(1+\frac{\sqrt{2}}{\kappa })`$ goes to unity. For finite $`\kappa `$ the general integral deforms the profile of the potential and the particular integral has a reduced amplitude.

Within Bardeen’s extension of the GL theory, Rickayzen’s formula is always recovered at low temperatures as $`\kappa `$ diverges with $`1/t^2`$. Since Rickayzen’s formula approaches the plain Bernoulli potential for $`t0`$, the presented derivation also reproduces London’s result.

### C Behavior for finite $`\kappa `$

As already shown, for the extreme type-II superconductor, $`\kappa \mathrm{}`$, the general integral vanishes as $`1/\kappa `$ and far from the surface it decays faster than the particular integral. The Bernoulli potential thus extends on the scale $`\lambda /2`$.

For the finite GL parameter in the region $`\kappa >\sqrt{2}`$ the overall picture is rather similar. The general integral is appreciable only close to the surface so that the scale on which the Bernoulli potential extends is still $`\lambda /2`$. Besides, the amplitude of the particular integral is enhanced by the factor $`1/(12/\kappa ^2)`$.

For the region $`\kappa <\sqrt{2}`$, the role of the general and particular integrals are reversed. First of all, the amplitude of the general integral is larger than the amplitude of the particular integral. Since the general integral also decays more slowly in this case, the Bernoulli potential is dominated by the general integral and extends on the scale $`\xi /\sqrt{2}`$. The reversed role is also supported by the fact that the signs of both parts are opposite as compared to the case $`\kappa >\sqrt{2}`$. This sign reversal appears due to the enhancement factor $`1/(12/\kappa ^2)`$.

Apparently, both components of $`\delta \phi `$ diverge as $`\kappa `$ approaches $`\sqrt{2}`$. Their sum remains regular, however. For this particular case the scale of both contributions is identical, namely $`\lambda /2`$. It is advantageous to use expression (23) to obtain the asymptotic form of the Bernoulli potential

$$\underset{\kappa \sqrt{2}}{lim}e\delta \phi =\frac{m}{4}v^2\left(\frac{n_s}{n}+4\frac{n_n}{n}\frac{\mathrm{ln}T_c}{\mathrm{ln}n}\right)\left(1+\frac{2x}{\lambda }\right).$$
(26)
The Bernoulli potentials for different values of the magnetic field are shown in Fig. 2. The limit of low magnetic fields agrees with the analytical formula (25), of course. One can see that for the two lowest fields $`B=0.01`$ and $`B=0.1`$, the potential keeps its profile while its magnitude scales with $`B^2`$. For magnetic fields close to the critical value $`B_{c2}0.34`$, the linear theory does not apply.

### D Charge profile

The charge density results from the Bernoulli potential (23) and the Poisson equation (1) as

$$\rho =\frac{2eϵ_0B^2}{m\left(1\frac{2}{\kappa ^2}\right)}(\frac{n_s}{n}+4\frac{n_n}{n}\frac{\mathrm{ln}T_c}{\mathrm{ln}n})(\mathrm{e}^{2x/\lambda }\frac{\kappa }{\sqrt{2}}\mathrm{e}^{\sqrt{2}x/\xi }).$$
(27)
Note that the relative amplitude of the two contributions is reciprocal to the relative amplitude of the potentials. Integrating from zero to infinity one can check that the total charge is zero, as it is required by the charge neutrality.

The resulting charge density is small compared to the total density of electrons $`en`$. The ratio of the amplitude of (27) to the total electron density can be written as

$$\frac{\rho }{en}\frac{ϵ_0B^2}{mn}=\frac{B^2}{\mu _0n}\frac{1}{mc^2}.$$
(28)
Even for upper estimates of the magnetic field by the critical value, $`BB_c`$, the factor (28) is extremely small. For niobium $`B^2/\mu _0=\frac{1}{2}\gamma T_c^2=3.2\times 10^4`$ J/m<sup>3</sup>, while $`mc^210^{13}`$ J. This suggests that the maximum charge density will be of the order of $`10^{18}`$ electrons per cubic meter. This is by ten orders of magnitude smaller than the electron density of niobium $`n=2.2\times 10^{28}`$ m<sup>-3</sup>. This small value of the accumulated or depleted charge justifies to ignore the charge profile in the Maxwell equation (5) and the change of material parameters like $`\gamma `$, $`n`$ and $`T_c`$ in the GL equation (4).

Similarly to the potential, the charge profile reflects two scales, $`\lambda /2`$ and $`\xi /\sqrt{2}`$. Before we analyze its properties for various values of the GL parameter $`\kappa `$, we want to discuss a few general features. First, the surface value of the charge, obtained for $`x=0`$ in (27), is always negative, i.e. the charge carriers are depleted. We call the layer of the negative charge the surface charge. Second, in the bulk sufficiently far from the surface the charge is positive, i.e., the charge carriers are accumulated. We call the region of positive charge the bulk charge. Third, the width $`w`$ of the surface is given by $`\rho (w)=0`$. From (27) follows

$$w=\frac{\lambda }{2}\frac{\mathrm{ln}\frac{\kappa }{\sqrt{2}}}{\frac{\kappa }{\sqrt{2}}1}.$$
(29)
In the extreme type-II superconductor, $`\kappa \mathrm{}`$, the surface charge is formed by the contribution on the scale of the GL coherence length $`\xi `$. The width of the surface goes to a value $`w\frac{\xi }{\sqrt{2}}\mathrm{ln}\frac{\kappa }{\sqrt{2}}`$. The bulk charge extends on the scale of the London penetration depth as it is known from the classical picture.

For the limiting case $`\kappa \sqrt{2}`$ the width of the surface charge is $`\lambda /2`$. The charge density has the profile

$$\rho =\frac{eϵ_0B^2}{m}\left(\frac{n_s}{n}+4\frac{n_n}{n}\frac{\mathrm{ln}T_c}{\mathrm{ln}n}\right)\mathrm{e}^{2x/\lambda }\left(1\frac{2x}{\lambda }\right).$$
(30)
Note the different sign inside the last parentheses compared to the Bernoulli potential (26). Since $`\lambda /2=\xi /\sqrt{2}`$ one cannot associate the surface and the bulk charge to the GL coherence length $`\xi `$ or to $`\lambda `$.

For $`\kappa <\sqrt{2}`$, the surface charge is formed by the contribution on the scale of the London penetration depth. For $`\kappa \sqrt{2}`$, the width of the surface charge is $`w\frac{\lambda }{2}\mathrm{ln}\frac{\sqrt{2}}{\kappa }`$. The bulk charge extends on the scale of the GL coherence length $`\xi `$ as one can see from (27).

## IV Strong magnetic field

In strong magnetic fields the GL wave function is suppressed in the vicinity of the surface which has to be accounted for in the Maxwell equation. In this case one has to face the fact that the system of equations (4) and (5) is nonlinear. We present only a few numerical solutions to point out some features typical for strong magnetic fields.

The nonlinear effects in strong magnetic fields follow from a deviation of the wave function from its bulk value. In the dimensionless representation used in Fig. 3 the bulk value is $`\psi _{\mathrm{}}=\sqrt{n/2}\sqrt{1t^4}0.6`$. For the lowest field $`B=0.01`$, the deviation is nearly zero on the scale of the graph. Also for $`B=0.1`$ the approximation $`|\delta \psi |\psi _{\mathrm{}}`$ is justified. For higher fields the deviation becomes appreciable.

The suppression of the wave function at the surface shown in Fig. 3 affects the Bernoulli potential by two different mechanisms. First, the screening current is reduced at the surface so that the magnetic field penetrates deeper into the superconductor. This feature can be seen in Fig. 2, however, it is better visible in the profile of the charge density shown in Fig. 1, as a widening of the surface layer.

Second, the thermodynamic contributions to the Bernoulli potential are nonlinear in the wave function, see (7). In contrast, the linearized approximation of the Bernoulli potential (23) or (25) does not depend on the density derivative of the linear coefficient of the specific heat, $`\gamma /n`$, included in the derivative of the condensation energy $`\frac{1}{4}\gamma T_c^2`$. Beyond the linearized approximation, this derivative contributes as demonstrated in Fig. 4 for parameters of niobium.

Comparing the contribution of $`\gamma /n`$ with the total charge density shown in Fig. 1, one can see that this particular nonlinear mechanism is rather small giving less than 3% of the total charge density. This small value justifies the approximations using only the term proportional to $`T_c/n`$.

## V Conclusions

In conclusion, we have shown that the Bernoulli potential in superconductors can be discussed by the charge build up in the region between the surface and $`max[\xi /\sqrt{2},\lambda /2]`$. The thinner depleted charge region carries the surface charge. In contrast to former theories which assumed that the surface charge is localized on the scale of Thomas-Fermi screening length $`\lambda _{\mathrm{TF}}`$, we find that the surface charge extends over a range $`L=min[\xi /\sqrt{2},\lambda /2]`$. In fact, there is a nonzero contribution on the scale of $`\lambda _{\mathrm{TF}}`$, but of a negligibly small amplitude proportional to $`\lambda _{\mathrm{TF}}^2/L^2`$.

For extreme type-II superconductors we have confirmed the picture known already from London with the thermodynamic corrections by Rickayzen. The bulk charge extends on the scale of the London penetration depth $`\lambda /2`$. The surface charge is localized on the scale of the GL coherence length $`\xi /\sqrt{2}`$ which is negligible in this limit anyway. This is in agreement with the classical treatment which neglects all gradient contributions.

In type-I or weak type-II superconductors, i.e for the GL parameter $`\kappa <\sqrt{2}`$, one finds the opposite situation. The surface charge is localized on the scale of the London penetration depth $`\lambda `$ while the bulk extends on the scale of the GL coherence length $`\xi /\sqrt{2}`$. In this case the gradient contributions are dominant and local London-type theories naturally fail.

In strong magnetic fields the Bernoulli potential becomes a non-quadratic function of the magnetic field. This feature parallels the nonlinear susceptibility as it is dominated by the enhanced penetration of strong magnetic fields into superconductors. There is an additional thermodynamic correction absent in low magnetic fields, however, for realistic material parameters (like for niobium) it accounts for less than 3% of the charge density. Thus the approximations used in  are justified.

Finally we remind that the potential $`\varphi `$ discussed here does not include the surface dipole which affects the potential seen outside the sample. We will discuss this contribution in a forthcoming paper.

###### Acknowledgements.

This work was supported by MŠMT program Kontakt ME601 and GAČR 202/03/0410, GAAV A1010312 grants. The European (ESF) program VORTEX is also acknowledged.


text:
# Iron Emission in z ≈ 6 QSOs and its Possible Implications

## 1. Introduction

The relative abundances of iron and $`\alpha `$-process elements in QSOs could provide an important constraint on the star-formation histories of their host galaxies (e.g. Yoshii, Tsujimoto & Kawara 1998; Korista et al., these proceedings). We report here the results of a Cycle 11 Hubble Space Telescope program to search for Fe II emission in five z $``$ 6 QSOs discovered in the Sloan Digital Sky Survey using the Near Infrared Camera and Multi-Object Spectrometer (NICMOS), and discuss the possible implications of our findings. The results for the first three objects observed in this program are also presented in Freudling, Corbin & Korista (2003).

## 2. Observations & Results

Observations of our sample objects were obtained between 2002 October 25 and 2003 June 19 using the NICMOS grism G141, with a nominal resolution of 200 pixel<sup>-1</sup>. This grism offers spectral coverage between approximately 1.1 $`\mu `$m $``$ 1.9 $`\mu `$m, and HST observations avoid the telluric absorption between the H and K bands. Total integration times for each object were approximately 40 minutes, and consisted of four separate integrations with the QSOs placed on each of the NICMOS Camera 3 detector quadrants in order to minimize pixel-to-pixel and large-scale sensitivity variations across the detector. Details of the calibration and reduction procedure are given in Freudling et al. (2003).

Our NICMOS spectra cover the portion of the rest-frame object spectra containing Al III $`\lambda `$1892, C III\] $`\lambda `$1909, the Fe II $`2500`$Å emission complex, and, except for the objects at z = 6.03 and z = 6.27, Mg II $`\lambda `$2800. In order to estimate the Fe II / Mg II ratio, we fit our final spectra as a combination of a power-law continuum, Fe II emission using a scaled version of the composite QSO spectrum of Zheng et al. (1997) as a template, and Gaussian profiles for the Al III $`\lambda `$1892, C III\] $`\lambda `$1909 and Mg II $`\lambda `$2800 lines. To compare our measurements of the Fe II / Mg II ratio with those measured for objects at lower redshifts, we apply a scaling factor to account for the Fe II emission out to 3300Å (rest), which our spectra do not cover (see Freudling et al. 2003). For SDSS J1306+0356 (z = 6.03) and SDSS J1030+0524 (z = 6.27), we estimate the flux in Mg II $`\lambda `$2800 from that measured in C III\] $`\lambda `$1909, using a Mg II $`\lambda `$2800 / C III\] $`\lambda `$1909 ratio of 1.36 $`\pm `$ 0.71, measured from a large sample of QSOs at z $``$ 2 (Brotherton et al. 1994). This assumes a similar ratio in our sample objects, which is reasonable given that their spectra near Ly$`\alpha `$ do not show any anomalous line strengths (e.g. Fan et al. 2001; Pentericci et al. 2002), and that both C and Mg are $`\alpha `$-process elements.

Our spectra and best fits to them are shown in Figure 1. Table 1 presents the corresponding scaled values of the Fe II / Mg II flux ratios, their uncertainties, and the redshifts we measure from the best fits to the emission lines. Our measurement of the ratio in SDSS J1208+0010 is very uncertain. The spectrum of Iwamuro et al. (2002) shows the Mg II profile to be very narrow, and it is unresolved in our spectrum, making it difficult to separate from the Fe II emission. We note that while the Fe II $`2500`$Å complex is weak in both SDSS J1306+0356 and SDSS J1030+0524, our best fits still yield some flux in it.

Our Fe II / Mg II flux ratios fall within the range measured for objects at lower redshifts (e.g. Iwamuro et al. 2002; Dietrich et al. 2002). Barth et al. (2003, and these proceedings) also find strong Fe II emission near Mg II $`\lambda `$2800 in the z = 6.4 QSO SDSS J1148+5251, and estimate a total Fe II / Mg II ratio within the same range. There is thus no evidence of a change in this ratio with redshift. Although the Fe II emission of AGN has proven difficult to model (see Baldwin et al. these proceedings), these ratios are consistent with Fe and Mg abundances near or above the solar level (Wills, Netzer & Wills 1985).

## 3. Discussion

If the iron detected in z $``$ 6 QSOs were produced mainly by SNe Ia, the evidence that it has reached solar and super-solar abundance levels has several important implications. First, the galaxy mass / metallicity relation indicates that the host galaxies of the QSOs are very massive, possibly the progenitors of giant ellipticals (see Hamann & Ferland 1999 and Fan et al., these proceedings). Such massive objects thus formed within $``$ 1 Gyr of the Big Bang. Second, recent calculations of SNe Ia formation and ISM enrichment timescales (Friaca & Terlevich 1998) indicate that solar Fe levels can be reached within 0.5 to 0.8 Gyr after the formation of the progenitor stars. Under currently favored cosmologies (h $``$ 0.7, $`\mathrm{\Omega }_\mathrm{\Lambda }`$ $``$ 0.73, $`\mathrm{\Omega }_M`$ $``$ 0.27) our results imply that the progenitor stars formed at z $``$ 20 $`\pm `$ 10 (see Freudling et al. 2003). This is consistent with the estimate of the first reionization epoch made from the polarization of the cosmic microwave background (Bennett et al. 2003). Finally, indirect and direct (Haiman & Cen 2002) constraints on the ages of z $``$ 6 QSOs indicate that they reached their present luminosities near their observed redshifts. The evidence that the stars of their host galaxies formed at higher redshifts thus supports models of an evolutionary connection between nuclear star formation and the AGN phenomenon (e.g. Norman & Scoville 1988; Kauffmann & Haenelt 2000; Kawakatu & Umemura 2003).

## References

Barth, A.J., Martini, P., Nelson, C.H. & Ho, L.C. 2003, ApJ, 594, L95

Bennett, C.L., et al. 2003, ApJS, 148, 1

Brotherton, M. S., Wills, B.J., Steidel, C.C. & Sargent, W.L.W. 1994, ApJ, 423, 131

Dietrich, M., Appenzeller, I., Vestergaard, M., & Wagner, S.J. 2002, ApJ, 564, 581

Fan, X., et al. 2001, AJ, 122, 2833

Friaca, A.C.S. & Terlevich, R.J. 1998, MNRAS, 298, 399

Freudling, W., Corbin, M.R. & Korista, K.T. 2003, ApJ, 587, L67

Haiman, Z. & Cen, R. 2002, ApJ, 578, 702

Hamann, F. & Ferland, G. 1999, ARA&A, 37, 487

Iwamuro, F., Motohara, K., Maihara, T., Kimura, M., Yoshii, Y. & Doi, M. 2002, ApJ, 565, 63

Kauffmann, G., & Haenelt, M. 2000, MNRAS, 311, 576

Kawakatu, N. & Umemura, M. 2003, ApJ, 583, 85

Norman, C. & Scoville, N. 1988, ApJ, 332, 124

Pentericci, L., et al. 2002, AJ, 123, 2151

Wills, B., Netzer, H. & Wills, D. 1985, ApJ, 288, 94

Yoshii, Y., Tsujimoto, T., & Kawara, K. 1998, ApJ, 507, L113

Zheng, W., Kriss, G.A., Telfer, R.C., Grimes, J.P. & Davidsen, A.F. 1997, 475, 469