I am aware of the issues with nonlinear functions of quantum fields. Those need to be dealt with by using the appropriate renormalization at the computational stage. I just wanted to make sure that given a solution to the computational problem (admittedly the more difficult one), that there are no further AC type difficulties in defining the theory.

I inverted the variance by accident--- I meant inverse variance is k^2. This is the typical free bosonic quantum field variance, and it is the same as a Boltzmann distribution for an elastic sheet. The inverse k^2 variance is still irregular at high frequencies at high dimensions, it is only continuous (Brownian) in 1d, and somewhat regular in dimension 2.

Yes on everything. The only topology I was thinking about is what you call the topology generated by the encoding. The only sticking point left is the you mention about almost everywhere convergence.

Sufficient to prove that the correlation functions exist (the Schwinger functions of sheffield's paper). Sorry for being blunt. If every subset is measurable, and the full space has measure 1, then any real valued function on the distributions you generate has an expectation value. All of these things are constructed in Sheffield, using a measurability result of Gross. But you don't need Gross if you have Solovay, so do you need Gross at all?

This answer is too trivial to answer the question. Given any function from some distributions to R, like the correlation function of <AB> where A,B are both distribution dotted into test function, the expected value is given by the integral of the induced map from [0,1] to R in Solovay land. First you map [0,1] to distributions using the program, then you map back to R. You need to show that all these functions are measurable in the usual set theory, and this is not obvious from what is given here.

Do you know a general proof that this dinky sigma algebra is sufficient? Such a proof would completely answer the question. The proofs in the literature are always on a case-by-case basis, like theorem 3.2 in Sheffield's paper, constructing the measure in a special case for Gaussian free fields, not for a general convergent random computation. Using these methods, you would need to work hard to demonstrate the existence of the measure for some other case. But there are clearly no issues if the measure is defined on all subsets of U, and this suggests that there should be a uniform solution.

The construction of theorem 2.3 in the Sheffield paper is what I want to avoid. This is a theorem of Gross which is cited, which constructs a probability measure which has the properties of the random picking measure. This theorem is trivial in Solovay-land, because the definition in the statement of the theorem automatically constructs the measure, but it is obviously considered nontrivial by Sheffield et. al. Is there a way to transfer the trivial proof to the usual universe, and avoid this Gross thing.

It seems very unlikely to me that you can extend the measure in the presence of choice to arbitrary subsets, precisely because the measure has certain translation properties which should allow a Vitali set (although I didn't do an explicit construction).

The question is as follows: you can define the random free field (for example) by picking all Fourier components as Gaussian random with width $k^2/L^2$. This is a complete definition in Solovay universe. Is it a complete definition in the standard universe?

@Gerhard: The axiom of choice is why you can't define measures by random picking. If you have a random picking, in the absence of choice, you can define the measure of a set S as the probability that the pick lands in S. This is the definition of random forcing, and this kind of random forcing kills choice. I want to know if the full Solovay machine is necessary, or if there is a substitute for this very simple construction. "Topos" is just a logicophobe's universe, so you can switch out universe for topos if you want.

@Qiaochu: The algebra of random fields is a useful surrogate for the usual examples in 4d, but if you consider a nonlinear sigma model, it is difficult to define the sum of target space variables because the random fields take values in a manifold without an obvious algebra. But it is still possible to heuristically define the picking algorithm, and in Solovay land this defines the measure. I don't think any language other than Solovay set-theory is necessary (people sometimes use a noncanonical embedding of the target space into R^n to get random variable algebras, but this is unnatural).

Measure theory is the standard language for probability/integration, and quantum fields are defined by probability/integration. The Solovay universe just guarantees that the Lebesgue measure for sets made without AC coincides with the Monte-Carlo definition of measure (the measure of S is the probability of a randomly picked number landing in x), and Monte-Carlo is how you compute quantum fields. What other language is there to use?

Thanks, sorry for the lapse. I must confess that it was initially surprising to me that V double dual is V (assuming probability is not contradictory, which I think one always should). The argument I found is too ad-hoc though--- there should be a simple non-measurable set. I will clean the answer up to remove the redundant assumption.