For an energy-conserving strong spherical shock wave expanding into mass density $C{r}^{-\beta }$, $0\le \beta <3$, dimensional analysis gives the displayed radius law. Neglect ambient pressure, radiation losses and gravity in this blast-dominated approximation. Write $u=\dot{R}U(\xi )$, $\rho =C{R}^{-\beta }D(\xi )$ and $p=C{R}^{-\beta }{\dot{R}}^{2}P(\xi )$, with $\xi =r/R$. The radial continuity equation, momentum equation and adiabatic pressure equation reduce toThe Strong-shock Rankine-Hugoniot conditions give $U(1)=P(1)=2/(\gamma +1)$ and $D(1)=(\gamma +1)/(\gamma -1)$. The explosion energy fixes the radius coefficient through $E=4\pi C{R}^{3-\beta }{\dot{R}}^2{\int }_0^1[D{U}^2/2+P/(\gamma -1)]{\xi }^{2}d\xi$.

Let a strong shock wave of radius $R$ and speed $V$ sweep a uniform mass density ${\rho }_0$ into a shell of mass $4\pi {\rho }_0{R}^3/3$ and speed $2V/(\gamma +1)$. If the cavity pressure is $\alpha$ times the immediate post-shock pressure, shell momentum balance gives $R\dot{V}=3(\alpha -1)V^2$. Constant total energy gives $R^3{V}^2=\mathrm{constant}$ and hence $\alpha =1/2$. Including shell internal and kinetic energy, and treating the cavity volume as $4\pi R^3/3$ to thin-shell accuracy, yields $R=\xi (E/{\rho }_0{)}^{1/5}{t}^{2/5}$ with ${\xi }^5=75(\gamma -1)(\gamma +1{)}^2/[16\pi (5\gamma -3)]$. This coefficient is approximate; resolving the shell's finite volume changes it.

An inductor is an electrical circuit component designed to provide self-inductance, often a coil such as a solenoid. An ideal linear inductor has constant $L>0$ and zero electrical resistance. Its stored magnetic energy, with zero chosen at zero electric current, isFor self-inductance $0.5\mathrm{H}$ and electric current $3\mathrm{A}$, this gives $U=2.25\mathrm{J}$. Unlike Joule heating, ideal storage is recoverable: the inductor can return energy to an electrical circuit when its electric current decreases. ^[ref].

The short derivation uses the terminal convention in self-inductance. The power absorbed by an ideal inductor isStarting from zero electric current, the integral of this power givesPositive $P_L$ increases stored magnetic energy; negative $P_L$ returns energy. At constant electric current $3\mathrm{A}$ in the example, $P_L=0$ and induced electromotive force is zero, but $U=2.25\mathrm{J}$ still resides in the magnetic field. The battery in the steady RL circuit supplies Joule heating in the electrical resistance, rather than further increasing the inductor's magnetic energy.

During the closed-loop release in RL circuit, stored magnetic energy plus accumulated Joule heating stays $2.25\mathrm{J}$. A real coil also has electrical resistance, so its Joule heating must be included separately from ideal inductor storage. The constant-$L$ formulas assume a fixed linear magnetic response.

Formal verification uses machine-checked formal proofs to establish functional correctness: the C implementation of verified seL4 configurations conforms to its formal specification. Binary correctness connects compiled machine code to that C behaviour where supported. Separate security formal proofs cover integrity, resource-access availability and confidentiality under their configuration requirements; these properties are not all available in every configuration. For example, the documented confidentiality theorem separates scheduler security domains rather than arbitrary pairs of software threads. ^[ref]

The documented assumptions include correct hardware, selected handwritten machine-interface code, correct boot state, translation lookaside buffer and memory cache management, and noninterfering or trusted DMA. The confidentiality result covers information channels in its model; the assumptions page explicitly excludes timing channels from that coverage. ^[ref]

Return to READ(7, 9, 0, 4). Correct IPC delivery does not establish that the service looked up the right file, returned LIME, or ever replied. A service can produce an incorrect payload while the operating-system kernel exactly follows its formal specification. The formal proofs therefore do not automatically prove all user-space services, nor turn the resource-access availability theorem into a guarantee that this file read completes. The verified foundation supports further algorithm correctness and system reasoning; the service protocol and its recovery obligations still need their own justification.

// Destination: computer-science.bigb

The exterior of an unknot is a solid torus. Inclusion of its boundary kills exactly the primitive Seifert longitude, so every essential simple closed curve bounding a disk in that exterior is isotopic, as an unoriented curve, to that longitude. The bounding disk need not avoid other link components.

A thermocouple uses two different electrical conductors and the Seebeck effect to infer a measuring-junction temperature from a voltage and a known reference temperature. The reference material and the reference temperature are distinct choices: B specifies the comparison Seebeck coefficient, while $T_c$ specifies the lower limit of the integral. The two-material experiment in Seebeck effect gives the geometry, sign convention, and calibration limitations.

The useful measurement is a pair: the raw terminal electric potential difference and the thermocouple reference junction temperature. For the A-positive terminal order and homogeneous-wire assumptions of Seebeck effect, write the open-circuit electromotive force asHere $T_h$ is the thermocouple measuring junction temperature and $T_c$ is the common temperature of the reference connections. The subscript $h$ names the measuring end; it need not be hotter. A voltmeter senses the complete connected thermoelectric path through the wires and its leads, in the electrochemical potential convention already described under Seebeck effect. It does not measure an absolute temperature, the individual Seebeck coefficient of A, or an isolated contact electric potential.

The Seebeck coefficient $S(T)$ quantifies the thermoelectric voltage response per small temperature difference at zero electric current. Use $S=-dV/dT$ along a homogeneous material, with voltage understood through electrochemical potential. Its units are volts per kelvin, commonly $\mu V/K$. The word thermopower is also used, despite this being a voltage response rather than power; some authors use that word for $|S|$, so check their convention. ^[ref].

For the A-minus-B terminal order in the Seebeck effect experiment,Thus a small temperature difference around $T_0$ gives $V_{AB}\approx [S_A(T_0)-S_B(T_0)]\Delta T$. The finite-interval ratio $V_{AB}/\Delta T$ is an average of the coefficient difference, not necessarily its value at either endpoint. Ordinary two-material measurements determine a relative Seebeck coefficient: to recover $S_A$ from the measured difference, add a separately known $S_B$. Neither the choice of a zero for voltage nor the use of a familiar reference material makes $S_B$ identically zero.

A concrete research example is Martin and colleagues' 2021 certification experiment. They measured small temperature differences and voltages on six silicon–germanium specimens at 13 base temperatures between $295$ and $900\mathrm{K}$. At each setting they acquired 40 voltage-and-temperature-difference pairs and used linear regression with a free intercept, so a constant voltage offset did not become part of the slope. Platinum voltage leads required a reference-material correction; their terminal order gave $S_{\mathrm{measured}}=S_{\mathrm{Pt}}-S_{\mathrm{specimen}}$, hence $S_{\mathrm{specimen}}=S_{\mathrm{Pt}}-S_{\mathrm{measured}}$. This is an actual measurement protocol, unlike the toy plot above. ^[ref].

Microscopically, a temperature gradient changes charge carrier transport until an opposing electrical response balances it at zero net electric current. In the usual simple semiconductor picture, electrons and electron holes give opposite Seebeck coefficient signs, and their contributions are weighted by their electrical conductivities. The Seebeck coefficient is a transport property: density of states alone does not determine it, since carrier motion and scattering also matter. Its usefulness extends beyond temperature sensing to diagnosing which carriers transport electric charge. ^[ref].

For downward settling velocity magnitude $W_s>0$ and eddy diffusivity ${\kappa }_T=Kz$, the total upward particle flux is $J=-W_s\varphi -Kz{\varphi }_z$. A stationary profile tending to zero at infinity has $J=0$, giving the displayed power law. The exponent compares settling with turbulent mixing. It describes a region above the bed; entrainment from the bed and viscous near-wall effects determine the reference concentration separately.

Second-order comprehension is a scheme asserting the existence of a second-order relation variable whose members are exactly the tuples satisfying a permitted formula:Here $R$ is not free in $\phi$, and the displayed individual and relation parameters are universally closed in each instance. Under full semantics for second-order logic, the selected external subset of $D^k$ is always available. Under Henkin semantics, the selected subset must lie in ${\mathcal{H}}_k$ for every allowed assignment of parameters. Different systems permit different formula classes: for example, arithmetical comprehension theory restricts comprehension to formulas without bound set variables, while still permitting set parameters. Consequently, the exact formula and parameter policy must accompany any claim that a restricted range satisfies second-order comprehension.

An existential second-order logic sentence has the formwhere each $R_i$ is a second-order relation variable of fixed finite arity $k_i$ and $\phi$ is a first-order sentence over the input first-order signature expanded by the $R_i$. The first-order sentence may contain both universal quantification and existential quantification over individuals; only the outer quantification over second-order relation variables is required to be existential. Under full semantics for second-order logic, truth means that some expansion by witness relations satisfies $\phi$.

For a fixed existential second-order logic sentence on a domain of cardinality $n$, the witnesses need ${\sum }_{i=1}^m{n}^{k_i}$ membership bits. The arities and the number of witnesses are constants because the sentence is fixed. After guessing those bits, a verifier evaluates the fixed first-order sentence by enumerating assignments to its finitely many individual variables, taking polynomial time. In the second-order encoding of three-colorability, the three witnesses require $3n$ bits, and the edge constraints can be checked over at most $n^2$ ordered vertex pairs. This is the logical form of the NP principle that a positive answer has a short complexity certificate.

The fixed-sentence qualification matters: it is the input first-order structure that varies, rather than an arbitrarily large formula supplied with each input. Fagin's theorem states the converse as well: every isomorphism-invariant NP property of finite relational first-order structures has such a description. The coloring example uses only unary second-order relation variables; the general theorem allows any fixed finite arities.

A second-order relation variable of arity $k\ge 1$ can be assigned a subset of the $k$-fold Cartesian product $D^k$; its application $R(x_1,\dots ,x_k)$ is true exactly when the tuple $(x_1,\dots ,x_k)$ belongs to that subset. Arity is the number of arguments, so a unary second-order relation variable is a predicate on individual objects. For a finite set $D$ of cardinality $n$, there are $n^k$ possible tuples and $2^{n^k}$ possible relations under full semantics for second-order logic. A relation is encoded by $n^k$ membership bits once the objects have been numbered; the number of possible witnesses can be exponential even when each witness has a short encoding.

For $(u,s),(v,t)$ in the second-order cone, the Cauchy-Schwarz inequality gives $u\cdot v+st\ge -\Vert u\Vert \Vert v\Vert +st\ge 0$. Thus the cone is contained in its dual cone. Conversely, if $s<\Vert u\Vert$ and $u\ne 0$, pairing $(u,s)$ with $(-u/\Vert u\Vert ,1)$ is negative. If $u=0$ and $s<0$, use $(0,1)$. Every point outside the cone therefore lies outside its dual, proving that it is a self-dual cone.

No cyclic heat engine exchanging heat only with two fixed thermal reservoirs at positive absolute temperatures $T_h>T_c$ can exceed the thermal efficiency of an engine whose cycle is a reversible thermodynamic process between them. All such reversible engines have the same thermal efficiency, regardless of their working substance. Let $Q_h>0$ be heat absorbed from the hot thermal reservoir and $Q_c>0$ the magnitude rejected to the cold one. ThenThe work convention is the one in the first law of thermodynamics: $W>0$ is net output by the engine. Use absolute thermodynamic temperatures, such as values in kelvin; ratios of readings in degree Celsius are invalid because their zero is shifted.

For $T_h=600\mathrm{K}$, $T_c=300\mathrm{K}$ and $Q_h=1000\mathrm{J}$, the maximum thermal efficiency is $50\%$. A reversible engine delivers $W=500\mathrm{J}$ and rejects $Q_c=500\mathrm{J}$. The thermal reservoirs have entropy changes $-1000/600$ and $+500/300\mathrm{J}{\mathrm{K}}^{-1}$, which cancel. The engine's own entropy change is zero over its thermodynamic cycle.

A short derivation now becomes transparent: the Second law of thermodynamics gives $-Q_h/T_h+Q_c/T_c\ge 0$, and the first law of thermodynamics gives $W=Q_h-Q_c$. Together they yield the bound and, more precisely,At fixed $Q_h,T_h,T_c$, every extra unit of total entropy production reduces output by $T_c$ units of energy. ^[ref]

Fixed thermal reservoirs are essential. Finite bodies cool and warm, so their initial temperature ratio cannot be used throughout an entire extraction process. As a computed contrast, the bodies with equal constant heat capacity in the entropy example would reach $T_f=\sqrt{600\times 300}=424.26\mathrm{K}$ if a reversible engine extracted work until their temperatures matched. Zero total entropy change gives this geometric mean; the first law of thermodynamics then gives $W_{\max }=C(600+300-2T_f)=5147.19\mathrm{J}$. Direct contact reaches $450\mathrm{K}$ and extracts no work.

Carnot's 1824 book asked whether the useful output of machines driven by heat was fundamentally limited and whether changing the working substance could improve that limit. Its reversible comparisons are the historical setting of Carnot's theorem. Carnot used the then-current caloric picture, treating heat as conserved in its passage through an engine; the modern balance $Q_h-Q_c=W$ should not be read back into that text.^[ref]

Rotate an ellipse with positive semiaxes $a,b$ about an axis a distance $r>a$ from its centre. For the parametrized surface $\sigma (u,v)=((r+a\sin u)\cos v,(r+a\sin u)\sin v,b\cos u)$, put $R=r+a\sin u$ and $D^2=a^2{\cos }^{2}u+b^2{\sin }^{2}u$. An outward unit normal is $N=(b\sin u\cos v,b\sin u\sin v,a\cos u)/D$. Direct differentiation gives the first fundamental form and second fundamental form, with the convention $I{I}_{ij}=⟨{\sigma }_{ij},N⟩$:Reversing the unit normal reverses $II$, but the Gaussian curvature $K=a{b}^2\sin u/(R{D}^4)$ is unchanged.

Differentiate the orthogonality of the unit normal to the two independent coordinate tangent vectors. If the second fundamental form vanishes, each derivative of the normal is orthogonal to both tangent vectors; differentiating its unit length also makes it orthogonal to the normal. Thus both normal derivatives vanish. On a connected parameter domain the normal is constant, and differentiating the position's scalar product with that constant normal proves the surface lies in a plane.

At every point its second fundamental form is a scalar multiple of its induced metric. Equivalently its shape operator is scalar, so all principal normal curvatures agree. For a three-dimensional hypersurface, $K=3\lambda$ and $K_{ab}{K}^{ab}=3{\lambda }^2$. The sign of its intrinsic scalar in a vacuum Lorentzian ambient space then follows from the Gauss equation for a nonnull hypersurface.

For an additive time series $X_t=T_t+S_t+{\epsilon }_t$ with period-$m$ seasonal component and ${\sum }_{j=1}^m{S}_j=0$, a centred average spanning one complete period removes the seasonal component while estimating the slowly varying trend. When $m$ is even, average two adjacent length-$m$ averages to centre the filter on an observation; the endpoints receive half the usual weights. Estimate each seasonal phase by averaging the corresponding detrended residuals across cycles, then subtract the mean of those phase averages to enforce the zero-sum convention. Multiplicative seasonality instead uses ratios and a mean-one convention. Repeated averaging is filter composition and induces serial dependence even from white noise.

Steric sea level change results from changes of seawater mass density at fixed ocean mass. To first order, thermal expansion gives $\Delta {\eta }_{\mathrm{thermal}}=\int \alpha \Delta Tdz$; changes in salinity give a halosteric contribution. The reference column, pressure and equation of state must be specified.

Eustatic sea level change is a change in global sea level associated with changes of ocean water amount or ocean-basin capacity. For contemporary climate budgets the relevant contribution is principally transfer of water between land and ocean, including melting grounded ice and changes in terrestrial water storage. It is distinct from steric sea level change.

With positive freshwater runoff $R$, net sea ice melt $I$ and precipitation $P$, and evaporation loss $E$, the ocean water-mass budget is $\dot{M}=R+I+P-E$. With salt-free ice and fixed total dissolved salt mass, mean salinity satisfies $\dot{S}/S=-\dot{M}/M$. Gross regional ice melt must not be substituted for net global melt without accounting for ice formation elsewhere and the averaging period.