Matching works

3 works

math.DS — Dynamical Systems

Counterexamples to the D-unstable-core conjecture for parameter-rich and elementary mass-action networks

Contributed by Michael Mislan

Two exact four-species counterexamples refute necessity of a D-unstable core for instability of a positive equilibrium. The first has five reactions, parameter-rich kinetics, an explicit generalized-mass-action equilibrium, and a rational Jacobian with eigenvalue 1/500 + (51/500)i. The second has six reactions, at most two molecules on each side of every reaction, no catalysts, and classical mass-action kinetics with fixed integer kinetic orders. At a positive rational equilibrium its Jacobian has integer entries and an unstable nonreal eigenvalue with real part between 0 and 5, certified by an exact shifted-quartic intermediate-value argument. The networks share a reactant incidence relation and 24 nonempty child selections. Exact symmetrization, triangular-block and cubic-factorization certificates show that every child matrix is D-nonunstable in both networks. A permanent zero eigenvalue in an exceptional child distinguishes D-noninstability from strict D-stability. Both counterexample theorems have Lean 4 proofs with Mathlib. A separate asymptotic calculation explains the elementary example through circulation and a fast branching coordinate. The results establish strict linear instability, without asserting a Hopf bifurcation or periodic orbit.

Primarily AI-generated textHuman understanding: some partsD-unstable coresLean formalizationchemical reaction networksclassical mass actioncounterexampleelementary bimolecular reactionsgeneralized mass actionparameter-rich kinetics

math.DS — Dynamical Systems

A critical-point criterion for D-stability in every dimension

Contributed by Michael Mislan

A real square matrix A is D-stable if DA is Hurwitz for every positive diagonal matrix D. Applying the critical-point method to Johnson’s contact variety establishes that, in every dimension and for every positive choice of barrier weights, D-stability is equivalent to Hurwitz stability and absence of positive solutions of an explicit principal-minor Fritz–John system. In dimension five the system separates into Lagrange and tangency branches; both equivalences are registered in Lean. Further results treat regular-contact persistence, the boundary of the D-stable set, stability under bounded time-scale ratios and the minimal destabilizing ratio. The finite decision procedure also uses conventional finiteness and termination arguments and was executed exactly only in dimension three. For the five-dimensional Lagrange system the multihomogeneous Bézout number is 1200; 980 generic complex solutions were observed numerically. Worked examples include a Lotka–Volterra community, a published refinery-column gain matrix and an exactly recovered benchmark window. Formal statements, conventional arguments, exact certificates and numerical illustrations are distinguished throughout.

Primarily AI-generated textHuman understanding: some partsD-stabilityFritz-John conditionsLean formalizationcritical-point methoddiagonal scalingtime-scale robustness

cs.CC — Computational Complexity

Deciding D-stability is coNP-hard

Contributed by Michael Mislan

The computational difficulty of D-stability, raised by Chen, Fan and Yu (1995, doi:10.1016/0167-6911(94)00036-U), is addressed by an explicit integer-matrix reduction from PARTITION. For positive weights of total 2T, the construction produces a matrix of order m + 4 that is D-stable exactly when no subset has weight T. When an equal split exists, some positive diagonal scaling has an eigenvalue with strictly positive real part. A Pell recursion supplies the parameters, with a logarithmic search bound and an explicit bound on every matrix entry. These bounds give polynomial binary output length. Together with the classical NP-completeness of PARTITION, the reduction yields coNP-hardness of D-stability and D-semistability, and NP-hardness of strict D-instability, even for a four-dimensional core with attachments at one coordinate. The hardness is in the weak sense for binary encoding. Running-time analysis and the trivial-instance cases are treated conventionally; registered Lean statements verify the explicit arithmetic encoding, bounds and promise dichotomy.

Primarily AI-generated textHuman understanding: some partsD-stabilityLean formalizationPARTITIONPell equationcoNP-hardnessdiagonal scaling

Advanced search

Text
Human understanding
Linked formalizations