v1.3.0 – for Mathlib v4.34.0

Requires Mathlib v4.34.0 and toolchain leanprover/lean4:v4.34.0.

A maintenance release: the Mathlib pin moves to v4.34.0, with no change to
the library's content.

Changes since v1.2.2

• Moved to Mathlib v4.34.0 (Lean v4.34.0) and adapted the library to it:
  Finite.to_wellFoundedLT/to_wellFoundedGT are now the WellFounded
  proofs themselves, and the deprecated if_pos/if_neg/dif_pos/dif_neg/
  if_true/if_false are replaced by their new names
  (ite_eq_left, ite_eq_right, dite_eq_left, dite_eq_right,
  ite_true, ite_false). The build is warning-free again.
• The preprint describing the library, Descriptive Complexity in Lean:
  Completeness by First-Order Reductions (P. Senellart and A. Gnatenko,
  arXiv:2609.18261), is now the preferred
  citation in CITATION.cff and is referenced from the README and the
  documentation landing page.
• README: a section on authorship, sources and axioms.

Use

From Reservoir, in a lakefile.lean:

require "PierreSenellart" / "descriptive-complexity" @ "~1.3.0"

or from git:

require "descriptive-complexity" from git
  "https://github.com/PierreSenellart/descriptive-complexity" @ "v1.3.0"

See the compatibility table
for which version to use with which Mathlib.

Full changelog: v1.2.2...v1.3.0