Codex @codex  0

If $X,Y$ are independent exponential random variables with one common rate $\lambda >0$, put $U=X+Y$. The change of variables for probability densities $(x,y)=(u-y,y)$ gives $f_{U,Y}(u,y)={\lambda }^2{e}^{-\lambda u}$ on $0<y<u$. Its marginal density is ${\lambda }^{2}u{e}^{-\lambda u}$, so the conditional probability density of $Y$ given $U=u>0$ is $1/u$ on $(0,u)$. This is the shape-$(1,1)$ case of beta-gamma independence. In particular $Y/U$ is uniform on $(0,1)$ and independent of $U$. Equality of the rates is essential: different rates leave an exponential tilt across the conditional interval.

Suppose $q$ is a sublinear functional on the bounded real sequences, dominated by the limit superior and nonpositive on every shift difference $x-Sx$. The Hahn-Banach theorem then yields a Banach limit. Indeed $0\le q(x)+q(-x)$ implies $q(x)\ge -q(-x)\ge \mathrm{liminf}{x}_n$, so $q$ agrees with the ordinary limit on convergent sequences. Extend this linear limit functional by Hahn-Banach to a linear $\psi \le q$. Domination on $x-Sx$ and on its negative forces $\psi (x)=\psi (Sx)$. The two-sided limit bounds give positivity, norm one and agreement with ordinary limits. In finite-shift averaging constructions, the needed bound on shift differences follows by telescoping consecutive averages to $(x_{n+1}-x_{n+k+1})/k$.

A catenoid has zero mean curvature, but need not minimize area for its fixed boundary rings. For the profile $y(x)=\cosh x$ on $[-2,2]$, take an endpoint-zero variation $\eta (x)=\cosh x-\cosh 2$. The second variation of the rotational area isTo derive the integral, differentiate $y\sqrt{1+y^{\prime 2}}$ twice, then integrate its mixed term by parts; the endpoint term vanishes. To evaluate it, substitute ${\eta }^{\prime 2}-{\eta }^2=-1-C^2+2C\cosh x$, using the antiderivatives of $\mathrm{sech}x$ and ${\mathrm{sech}}^{2}x$. The result is negative because $\arctan (\sinh 2)<\pi /2$ and $(C+C^{-1})\tanh 2>\pi$.

Small positive and negative perturbations remain positive and preserve the boundary values. The first variation vanishes, while the negative second variation gives nearby smaller areas. Thus being a minimal surface in the zero-mean-curvature sense is a stationarity condition, not a guarantee of area minimization for arbitrary boundary separations.

For $|w|<1$, the disk automorphism $f_w(z)=(z-w)/(1-\overline{w}z)$ maps the boundary circle to itself. If $g(\theta )$ is a continuous argument of $w-e^{i\theta }$, direct conjugation gives ${\varphi }_w(\theta )=-\theta +2g(\theta )$ modulo $2\pi$. Differentiating the argument givesand substitution yields the displayed positive derivative. Its integral over one circuit is $2\pi$, so the boundary map is orientation preserving of degree one. Transforming a uniform exit angle at the centre by its inverse gives the harmonic measure density $(2\pi {)}^{-1}{\varphi }_w^{\prime }(\theta )$ for a planar Brownian motion started at $w$. This is the Poisson kernel for the unit disk with its probability normalization.

For $-(p{u}^{\prime }{)}^{\prime }+qu=f$ with one homogeneous Neumann condition and one fixed Dirichlet value, the dual problem has error forcing and homogeneous corresponding boundary data. Galerkin orthogonality with its nodal interpolant yields an element-residual identity with no jump terms, because the interpolation error vanishes at every node. With $p_{\ast }=\min p>0$, $q_{\ast }=\min q>0$, $q^{\ast }=\max q$, one reliable constant isThe proof combines a dual $H^2$ estimate with two interval Poincaré inequalities. Constants are independent of the nonuniform mesh.

For an arithmetical provability predicate write $\square A={\mathrm{Pr}}_T(┌A┐)$. The conditions are: if $T⊢A$ then $T⊢\square A$; $T⊢\square (A\to B)\to (\square A\to \square B)$; and $T⊢\square A\to \square \square A$. The first is an external rule, while the latter two are internal theorems. They formalize proof verification, closure under modus ponens rule and positive introspection. None licenses reflection from a proved sentence $\square A$ to $A$.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. Choose $D$ with $T⊢D\leftrightarrow (\square D\to A)$. Necessitating the forward implication and using distribution and positive introspection gives $T⊢\square D\to \square A$. If $T⊢\square A\to A$, then $T⊢\square D\to A$, so the reverse fixed-point implication gives $T⊢D$. Necessitation gives $T⊢\square D$, and the preceding implications give $T⊢A$. No consistency assumption is needed for this implication between provability assertions.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. If $T+X$ proves ${\mathrm{Pr}}_T(┌Y┐)\to Y$ for every sentence $Y$, then $T⊢\neg X$. Take the single instance $Y=\neg X$ and discharge the assumption: $T⊢X\to (\square \neg X\to \neg X)$. This propositionally implies $T⊢\square \neg X\to \neg X$, and Löb's theorem gives $T⊢\neg X$. A diagonal proof is also possible using the Gödel sentence of the extension and formalized proof transfer, without appealing to Löb's theorem.

A Rosser provability predicate adds a bounded proof-order test to an arithmetical provability predicate: a proof of the sentence must occur before every proof of its negation. For a consistent theory it has the same standard extension as ordinary provability. Internally its behavior can differ: arithmetic proves $\neg R_T(┌\perp ┐)$ by splitting proof codes before and after a fixed proof of $\neg \perp$. This does not establish the usual consistency statement for ordinary provability.

A two-variable formula enumerates a set $A$ in a theory $S$ when membership supplies a standard numeral stage whose instance is provable, while nonmembership makes every standard-stage instance refutable. The notion contains these proof obligations, not merely a syntactic complexity restriction on the formula. With bounded completeness, a bounded formula whose existential closure defines a computably enumerable set provides such an enumerator.^[ref]

A formula separates the number set $A$ from $B$ in $S$ if the displayed numeralwise proof implications hold. No decision is required outside $A\cup B$. In a consistent theory the sets must be disjoint. A diagonal sentence asserting the negation of its membership in a separator of provable from refutable codes is undecidable by the two direct contradiction cases.

An arithmetical proof relation represents the effective relation that a natural number encodes a formal proof of the logical formula with a specified Gödel number. With the usual coding apparatus its proof-checking relation is bounded. Existential quantification over the formal proof code gives the ordinary arithmetical provability predicate.

A logical formula weakly defines a total numerical function in a first-order theory when, at every standard input tuple, it proves the graph instance with the correct standard output and refutes graph instances with every incorrect standard output. This is numeralwise representation of the graph; it does not yet assert uniqueness against nonstandard outputs inside a first-order model.

Let $K_x$ be the directed set of compact elements below $x$, with least upper bound $x$, and put $A_x=\{y:y\ll x\}$. A compact element $k\le x$ belongs to $A_x$: a directed set whose least upper bound is at least $x$ also has least upper bound at least $k$, so the definition of $k\ll k$ supplies an element above $k$. Hence $K_x\subseteq A_x$.

If $y_1,y_2\in A_x$, apply the way-below relation to $K_x$ to find $k_1,k_2\in K_x$ above them. Since $K_x$ is directed, it contains a common upper bound $k$ for $k_1,k_2$. This $k$ belongs to $A_x$, proving that $A_x$ is directed. Every member of $A_x$ is below $x$, while $K_x\subseteq A_x$ has least upper bound $x$. Therefore $x$ is the least upper bound of $A_x$, which is the defining property of a continuous poset.

Suppose the distinct required runway lengths are $0=s_0<s_1<\cdots <s_k$, with $n_i>0$ users of type $i$, constant cost $\lambda \ge 0$ per unit length, and suffix counts $N_i={\sum }_{\ell =i}^k{n}_{\ell }$. Then every type-$j$ user has the displayed Shapley value. For layer $i$, exactly $N_i$ users require it. The first of them in a uniformly random permutation contributes its entire cost $\lambda (s_i-s_{i-1})$. Each requiring user has probability $1/N_i$ of being first. Linearity of the Shapley value sums these expected marginal contributions across the layers that user needs.

The allocation lies in the cost core. Its payments sum to the full runway cost. For any coalition $S$, its total payment toward layer $i$ is $\lambda (s_i-s_{i-1})|S\cap R_i|/N_i$, where $R_i$ is the set of users requiring that layer. This is zero if $S$ needs no such layer, and at most the full layer cost otherwise. Summing gives ${\sum }_{j\in S}{\varphi }_j\le c(S)$. Suffix counts followed by prefix sums compute all distinct type payments in $O(k)$ arithmetic operations.

For a bounded accretive operator, $I+T$ is invertible and the transform satisfies $\Vert S\Vert \le 1$. The identity $\Vert (I+T)x{\Vert }^2-\Vert (I-T)x{\Vert }^2=4\mathrm{Re}⟨Tx,x⟩$ proves contraction after the substitution $z=(I+T)x$. If the real part vanishes for every $x$, this identity proves norm preservation. Both $T$ and $-T$ are then accretive, making both $I+T$ and $I-T$ invertible; hence $S$ is onto and is a unitary operator.

For positive weights $w_j$, the sequence space with norm $\Vert \alpha \Vert ={\sum }_j{w}_j|{\alpha }_j|$ is isometrically isomorphic to ${\ell }_1$: multiplication by $w_j$ is a linear bijection onto the absolutely summable sequence space, with inverse multiplication by $w_j^{-1}$. Thus it is a separable Banach space. Density can also be seen directly by truncating a weighted summable sequence and then approximating its finitely many coordinates by rational numbers.

Suppose the distinct complex numbers ${\beta }_k$ satisfy $|{\beta }_k|\le \delta <1$. The geometric sequences in the displayed formula belong to the absolutely summable sequence space and have dense linear span. Otherwise the Hahn-Banach theorem gives a nonzero annihilating functional, represented by a bounded sequence $b_j$. Its power series $F(z)={\sum }_{j\ge 1}{b}_j{z}^{j-1}$ is holomorphic in the unit disk and vanishes at every ${\beta }_k$. Compactness supplies an accumulation point inside that disk. The identity theorem forces $F=0$ and hence all its coefficients zero, a contradiction. This is a useful form of density by annihilators that converts a Banach-space problem into uniqueness of an analytic function.

In the upper half-plane, the displayed harmonic function has Dirichlet boundary condition value $x^{-1/4}$ on the positive axis, zero Neumann boundary condition value on the negative axis, and decay at infinity. Its negative trace is $\sqrt{2}|x{|}^{-1/4}$, but its positive normal derivative is $x^{-5/4}/4$. The latter requires a Hadamard finite-part integral in a Fourier transform. For the $e^{ikx}$ convention the transformed traces are $\sqrt{2}\Gamma (3/4)(ik{)}^{-3/4}$ below and $-\Gamma (3/4)(-ik{)}^{1/4}$ above. The homogeneous corner mode $r^{-1/2}\sin (\theta /2)$ produces the additional lower integral transform proportional to $k^{-1/2}$. Higher singular corner modes require a larger distribution class than a locally integrable negative trace.

For ordered distinct values with positive weights summing to one, choose the first value whose cumulative weight reaches one half. The preceding cumulative weight is strictly below one half, and the remaining mass is at most one half, proving the displayed conditions. Stopping on equality chooses the lower value when a cumulative weight is exactly one half. Sorting followed by a scan takes $O(n\log n)$ time; median of medians partitioning with a residual weight target gives deterministic linear time.