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.

Complete symmetrized constant-coefficient evolution — Examples

1 · Prerequisites

2 · Summary

An exact positive-parameter choice for the corrected bulk-relaxation branch gives a characteristic speed greater than the reference speed. This parameter example is conditional mathematics, not an estimate of a material coefficient.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-adaptedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

Positive relaxation parameters can give superluminal characteristic speed

Example

Choose $n_{0}, T_{0}, h_{0}, τ, c > 0$ and $σ_{p 0} \in R$ , put $v_{0} = 1 / n_{0}$ , and on an open neighborhood $X \subset (0, \infty) \times R$ of $(v_{0}, σ_{p 0})$ define the $C^{2}$ local energy per marker

$e (v, σ_{p}) = \frac{h_{0}}{n_{0}} + T_{0} (σ_{p} - σ_{p 0}) + \frac{n_{0} h_{0}}{6} (v - v_{0})^{2} .$

Choose $X$ small enough that $v > 0$ and the local enthalpy density $h : = ϵ + p$ , with $n = 1 / v$ , $ϵ = n e$ , and $p = - e_{v}$ , remains positive. At the reference state, $T = e_{σ_{p}} = T_{0} > 0$ , $p_{0} = - e_{v} (v_{0}, σ_{p 0}) = 0$ , $ϵ_{0} = n_{0} e (v_{0}, σ_{p 0}) = h_{0}$ , and $e_{v v} (v_{0}, σ_{p 0}) = n_{0} h_{0} / 3$ . The local Gibbs response in Bulk linear relaxation energy, stability and causal speed therefore realizes $a_{s} = e_{v v} / (n_{0} h_{0}) = 1 / 3$ . Now set $ζ = τ h_{0}$ . All positivity hypotheses of that bulk linear branch hold, but its exact normal characteristic speed is $v_{b u l k} = c \sqrt{1 / 3 + 1} = 2 c / \sqrt{3} > c$ . With SI units, $h_{0}$ is in Pa and $τ$ in s, so $ζ$ is in Pa s. This is a parameterized mathematical model example, not a measurement or an estimate for a material.

Facts & Assumptions

Given: The constructed local state and positive parameters in the Example, with $h_{0}$ in Pa, $τ$ in s, $ζ = τ h_{0}$ in $P a s$ , and $c > 0$ the reference speed parameter.

[A1]

The only choice premise in the supplier chain is countable choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[A2]

At $(v_{0}, σ_{p 0})$ , $p_{0} = 0$ , $ϵ_{0} = h_{0}$ , $T_{0} > 0$ , and $e_{v v} = n_{0} h_{0} / 3 > 0$ ; by continuity, $X$ can be chosen open with $v > 0$ and $h > 0$ throughout.

[F1]

Bulk linear relaxation energy, stability and causal speed: under $a_{s}, h_{0}, ζ, τ > 0$ and the exact local Gibbs response, the branch speed is $v_{b u l k} = c \sqrt{a_{s} + ζ / (τ h_{0})}$ .

[F2]

Corrected bulk relaxation and exact extended entropy: every actual smooth solution of the corrected law and balances with $ζ, c, T > 0$ satisfies $\nabla_{a} S^{a} = Π^{2} / (ζ c T) \geq 0$ . This conditional entropy identity supplies no algebraic bound on the linear characteristic speed.

Verification

1.1A1A2F1givenalgebra

Direct differentiation of $e$ gives $e_{v} (v_{0}, σ_{p 0}) = 0$ and $e_{v v} (v_{0}, σ_{p 0}) = n_{0} h_{0} / 3$ . Thus [A2] verifies the local state's positive $n_{0}, T_{0}, h_{0}, e_{v v}$ hypotheses, and [F1] supplies $a_{s} = e_{v v} / (n_{0} h_{0}) = 1 / 3$ . The choice $ζ = τ h_{0}$ gives $ζ / (τ h_{0}) = 1$ , so all remaining strict positivity hypotheses of [F1] hold.

2.1F1F2step 1.1givenalgebra∎

Substitution gives $v_{b u l k} = c \sqrt{1 / 3 + 1} = 2 c / \sqrt{3}$ . Since $4 / 3 > 1$ and $c > 0$ , $2 c / \sqrt{3} > c$ . The separate entropy identity in [F2] is nonnegative whenever its actual-solution hypotheses hold, including $T > 0$ ; that conditional sign statement supplies no bound on this characteristic speed.