Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Continuum Heat Model — Examples

1 · Prerequisites

2 · Summary

These are constructed examples inside the adopted constant-coefficient Fourier model, not measured temperature records. The first computes a compatible nonuniform profile's mean and variance exactly, then applies the conditional relaxation theorem. The second shows that the model's positive Gaussian kernel produces an immediate nonzero perturbation throughout the rectangle from compactly supported initial data. That is a mathematical property of the diffusion equation, not an experimental assertion about signal speeds.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

A nonuniform insulated temperature profile relaxes to its mean

Physical scope

An exact initial-profile example inside the constant-capacity, constant-conductivity insulated rectangular model; it is a conditional calculation, not an observation.

Statement

Assume Countable Choice as in Constant-conductivity heat evolution on an insulated rectangle. Let $L_{i} > 0$ be lengths in metres and $Ω = \prod_{i = 1}^{3} (0, L_{i})$ . Let $c > 0$ be a constant volumetric heat capacity in $J m^{- 3} K^{- 1}$ , $k > 0$ a constant scalar conductivity in $W m^{- 1} K^{- 1}$ , and $u_{⋆}$ an arbitrary reference energy density in $J m^{- 3}$ , with $u (θ) = u_{⋆} + c θ$ as in Constant-conductivity heat evolution on an insulated rectangle. Let $T_{b}$ and $ϵ$ be temperatures in kelvins with $T_{b} > ϵ / 30 > 0$ . For $r \in [0, 1]$ set $h (r) = r^{2} (1 - r)^{2} - 1 / 30$ and prescribe $g (x) = T_{b} + ϵ h (x_{1} / L_{1}) (x \in \overline{Ω}) .$ Use its even $2 L_{i}$ -periodic extension in each coordinate as the initial datum on $R^{3}$ . The unique insulated heat solution has constant spatial mean $T_{b}$ and satisfies $\int_{Ω} ∣ T (x, t) - T_{b} ∣^{2} d x \leq \frac{ϵ^{2} ∣ Ω ∣}{2100} e^{- 2 (k / c) t / C_{Ω}}, C_{Ω} = \frac{3}{2} \max_{i} L_{i}^{2} .$ This gives an exactly computed initial variance and the conditional relaxation estimate of the model.

Facts & Assumptions

Given: Countable Choice; lengths $L_{i}$ in metres; $c, k, u_{⋆}, T_{b}, ϵ$ with the units and hypotheses in the Statement; the profile $h (r) = r^{2} (1 - r)^{2} - 1 / 30$ ; and the field $g (x) = T_{b} + ϵ h (x_{1} / L_{1})$ .

[A1]

Countable Choice is the explicit hypothesis used by the heat-evolution supplier The Axiom of Countable Choice ( ${A C}_{ω}$ ).

[F1]

Constant-conductivity heat evolution on an insulated rectangle: the even-periodic compatible initial field has the unique Gaussian-convolution heat solution with positive bounds and homogeneous Neumann faces.

[F2]

Exponential relaxation of the constant-conductivity Neumann heat model: for this solution, the mean is conserved and $E (t) \leq e^{- 2 (k / c) t / C_{Ω}} E (0)$ .

Example

The function $h$ is dimensionless, and $g$ has units of kelvins. The extension uses even reflection at each face and period $2 L_{i}$ ; the initial field is nonconstant but compatible with insulated walls.

Verification

1.1givenalgebra

Write $q (r) = r^{2} (1 - r)^{2}$ . Then $q^{'} (r) = 2 r (1 - r) (1 - 2 r)$ , so $q^{'} (0) = q^{'} (1) = 0$ , and $q^{''} (0) = q^{''} (1) = 2$ . Also $0 \leq q \leq 1 / 16$ on $[0, 1]$ . The constant and first two derivatives therefore match across the even-reflection and periodic seams; the extension is $C^{2}$ , with bounded uniformly continuous derivatives. Since $h = q - 1 / 30$ , its values lie in $[- 1 / 30, 7 / 240]$ , so $g \geq T_{b} - ϵ / 30 > 0$ .

1.2givenalgebra

Expand $q (r) = r^{2} - 2 r^{3} + r^{4}$ , so $\int_{0}^{1} q (r) d r = 1 / 3 - 1 / 2 + 1 / 5 = 1 / 30$ . Also $q (r)^{2} = r^{4} - 4 r^{5} + 6 r^{6} - 4 r^{7} + r^{8}$ , whence $\int_{0}^{1} q (r)^{2} d r = \frac{1}{5} - \frac{4}{6} + \frac{6}{7} - \frac{4}{8} + \frac{1}{9} = \frac{1}{630} .$ Therefore $\int_{0}^{1} h (r) d r = 0$ and $\int_{0}^{1} h (r)^{2} d r = \int_{0}^{1} (q - 1 / 30)^{2} d r = \frac{1}{630} - \frac{1}{900} = \frac{1}{2100} .$ Integrating over the other two coordinates now gives $\overline{g} = T_{b}$ and $E (0) = ϵ^{2} L_{2} L_{3} L_{1} / 2100 = ϵ^{2} ∣ Ω ∣ / 2100$ .

2.1A1F1F2step 1.1step 1.2∎

The profile satisfies every initial-data hypothesis of [F1]; its vanishing normal derivative follows from $q^{'} (0) = q^{'} (1) = 0$ . Apply [F1] for existence and [F2] with the computed $E (0)$ to obtain the stated conserved mean and decay bound. This is a deduction within the adopted continuum model.

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

The rectangular Fourier model has instantaneous spatial support

Physical scope

A mathematical support property of the constant-coefficient Fourier heat model on an insulated rectangle; it is not an observation or a claim about finite-speed physical signals.

Statement

Assume Countable Choice as in Constant-conductivity heat evolution on an insulated rectangle. Let $L_{i} > 0$ be lengths in metres and $Ω = \prod_{i = 1}^{3} (0, L_{i})$ . Let $c > 0$ be a constant volumetric heat capacity in $J m^{- 3} K^{- 1}$ , $k > 0$ a constant scalar conductivity in $W m^{- 1} K^{- 1}$ , and $u_{⋆}$ an arbitrary reference energy density in $J m^{- 3}$ , with $u (θ) = u_{⋆} + c θ$ as in Constant-conductivity heat evolution on an insulated rectangle. Choose $x_{c} = (L_{1} / 2, L_{2} / 2, L_{3} / 2)$ and a radius $r$ in metres with $0 < r < \frac{1}{2} \min_{i} L_{i}$ , and let $T_{b}, ϵ > 0$ be temperatures in kelvins. Define on $\overline{Ω}$ $ϕ (x) = {\begin{cases} (1 - ∣ x - x_{c} ∣^{2} / r^{2})^{3}, & ∣ x - x_{c} ∣ < r, \\ 0, & ∣ x - x_{c} ∣ \geq r . \end{cases}$ For $L > 0$ , define the even periodic fold $ρ_{L} : R \to [0, L]$ by $ρ_{L} (s) = s - 2 n L$ for $2 n L \leq s \leq (2 n + 1) L$ and $ρ_{L} (s) = (2 n + 2) L - s$ for $(2 n + 1) L \leq s \leq (2 n + 2) L$ , $n \in Z$ . Put $ϕ_{p e r} (x) = ϕ (ρ_{L_{1}} (x_{1}), ρ_{L_{2}} (x_{2}), ρ_{L_{3}} (x_{3}))$ and take $g = T_{b} + ϵ ϕ_{p e r}$ . In the constant- $c, k$ insulated Fourier model, the heat-kernel solution satisfies $T (x, t) - T_{b} = ϵ \int_{R^{3}} Γ (x - y, (k / c) t) ϕ_{p e r} (y) d y > 0$ for every interior $x \in Ω$ and every $t > 0$ , although the initial perturbation is supported in the compact ball $\overline{B} (x_{c}, r) \subset Ω$ . Thus the adopted diffusion model has no finite propagation speed for this temperature perturbation.

Facts & Assumptions

Given: Countable Choice; lengths $L_{i}$ and radius $r$ in metres; the constants $c, k, u_{⋆}, T_{b}, ϵ$ with the units and hypotheses in the Statement; and the centre $x_{c}$ and profile $ϕ$ defined there.

[A1]

Countable Choice is the explicit hypothesis carried by the heat-evolution supplier The Axiom of Countable Choice ( ${A C}_{ω}$ ).

[F1]

Constant-conductivity heat evolution on an insulated rectangle: under Countable Choice and the stated constant positive $c, k$ , a $C^{2}$ initial field $g : R^{3} \to (0, \infty)$ that is even in each coordinate and $2 L_{i}$ -periodic in coordinate $i$ , with every coordinate derivative through order two bounded and uniformly continuous and bounds $0 < T_{\min} \leq g \leq T_{\max} < \infty$ , has the stated insulated Gaussian-convolution solution. The Gaussian is strictly positive and has unit mass.

Example

The cutoff $ϕ$ is dimensionless, so $ϵ$ and $T_{b}$ are in kelvins. The perturbation is a constructed model profile, not measured data. It is zero outside a ball at $t = 0$ and is nonzero throughout the body for every positive time under the adopted Fourier equation.

Verification

1.1givenalgebra

Inside the ball write $h (x) = 1 - ∣ x - x_{c} ∣^{2} / r^{2}$ , so $ϕ = h^{3}$ . On the sphere $h = 0$ , the first derivatives $3 h^{2} \partial_{i} h$ and second derivatives $6 h (\partial_{i} h) (\partial_{j} h) + 3 h^{2} \partial_{i} \partial_{j} h$ tend to zero; outside the ball they are zero. Hence $ϕ$ is $C^{2}$ and nonnegative, and it is identically zero in a neighborhood of every face because $r < \frac{1}{2} \min_{i} L_{i}$ . The reflected periodic extension is therefore $C^{2}$ , bounded with bounded uniformly continuous derivatives through order two (by continuity and periodicity), and positive on the original open ball.

2.1A1F1step 1.1algebra

The initial field $g = T_{b} + ϵ ϕ_{p e r}$ satisfies $0 < T_{b} \leq g \leq T_{b} + ϵ$ and all the derivative and even-periodic hypotheses of [F1]. Unit mass of the Gaussian gives $T (x, t) - T_{b} = ϵ \int Γ (x - y, (k / c) t) ϕ_{p e r} (y) d y$ . For $t > 0$ and any $x \in Ω$ , the Gaussian $Γ (x - y, (k / c) t)$ is strictly positive on the ball. Choose a smaller closed ball on which the continuous $ϕ_{p e r}$ has a positive minimum; the Gaussian also has a positive minimum there. Its integral over that ball is positive, so the convolution in [F1] gives $T (x, t) - T_{b} > 0$ .

3.1step 1.1step 2.1given∎

At $t = 0$ , $ϕ_{p e r}$ restricted to $Ω$ vanishes outside $\overline{B} (x_{c}, r)$ , a proper compact subset of the rectangle, while step 2.1 shows the positive-time perturbation is nonzero at every interior point. This is instantaneous support growth in the specified diffusion model only.

Continuum Heat Model — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

A nonuniform insulated temperature profile relaxes to its mean

Statement

Facts & Assumptions

Example

Verification

The rectangular Fourier model has instantaneous spatial support

Statement

Facts & Assumptions

Example

Verification

Sources