v4.35.0

Built against Lean v4.35.0 and mathlib v4.35.0.

New

• Edge graphs as mathlib quivers: typed walks are Quiver.Paths, and the path category is isomorphic to mathlib's Paths. The path category's universal property is included.
• Flat path functors (Maths/Graph/FlatPathFunctor.lean): a walk with a return walk between flat vertices is an isomorphism (isoOfIsFlatAt). The fiber equivalences of flat transport and the units of flat labellings both come from it.
• Classical gain graphs, graphs of elements, the frustration index, and octagons.
• Active optimal certificates and fair worklist relaxation.
• Application capstones: certified reachability, timing, control radii, and sensor consistency.
• A fixed vocabulary, recorded in TERMINOLOGY.md with an index from classical, domain and retired names (subsolution, circuit, polarity, residual, …) to the canonical term and the module that develops it. Every module has a mathlib Tags section, so searches for phrases such as max-plus or Bellman operator find it.
• EdgeGraph.isStronglyConnected_iff_quiver identifies strong connectivity with mathlib's Quiver.IsStronglyConnected; slopeProd_eq_pathSlope and suffixSlopeSum_eq_pathRelaxationMass tie the edge-list accounting to the label-list accounting.

Changed

• Sections are relational morphisms out of the terminal transport. Transport.Simulation is renamed Transport.HomFor; Hom, LaxHom and OplaxHom are its cases for =, ≤ and ≥. Lax sections form a Moore family with a bundled closure operator.
• The core, graph, recursion, linear-programming and specialization layers were deduplicated against each other and against mathlib, removing about 1700 lines net across the release.
• Several results now take weaker hypotheses: nonnegative instead of positive slopes in the weighted-defect obstruction, P ≠ 1 instead of P < 1 in the wrap identity, no positive-slope hypothesis where an expansive gauge already implies it, and finite-inequality compatibility over any linearly ordered field. Strong connectivity no longer takes a base vertex, so the additive exactness criterion now also covers the empty vertex type.
• Docstrings that misstated the mathematics are corrected: the strongly connected component in EdgeEndpointsLinkedTo, the sign of defect against LP slack, the sub/super wording on subeigenvectors, the "admissible eigenvalues" ray, and a theorem of the alternative that was labelled strong duality.
• Walk-only notions moved to Maths/Graph/, so these are renamed:
  • IsSimpleCycle → EdgeGraph.Walk.IsSimpleCycle
  • exists_walk_length_eq → EdgeGraph.exists_walk_length_eq
  • exists_source_eq → EdgeGraph.exists_source_eq
  • walkSum_coboundary → Maths.walkSum_coboundary
  • IsFlatAt keeps its name and is now defined in the graph layer.

Terminology pass

Identifiers that contradicted the vocabulary are renamed. MIGRATION.md has the full table, including lemma families.

Namespaces and modules

• Maths.MaxPlusPotential, Maths.MixedAdditiveTransport, Maths.CycleCoboundary → Maths.AdditiveTransport, keeping the short names (mirroring Maths.MaxAffineTransport)
• The finite-inequality alternative moved from the root namespace into Maths.FiniteInequality; finiteInequalityMatrix → FiniteInequality.finMatrix, finiteInequality_feasible_iff → isFeasible_finMatrix_iff
• Module MaxAffine.CycleSlack → MaxAffine.CycleRelaxation
• Module MaxAffine.AnchoredEigenvalue → MaxAffine.ReachableLowerBounds
• Module Additive.Circuits → Additive.SignedCycles

Farkas certificates (one name for the nonnegative balanced combination witnessing infeasibility)

• LinearProgramming.IsCertificate, HasCertificate → IsFarkasCertificate, HasFarkasCertificate
• exists_potential_or_nonnegative_incompatibility → FiniteInequality.exists_potential_or_farkasCertificate
• exists_potential_iff_no_nonnegative_incompatibility → FiniteInequality.exists_potential_iff_no_farkasCertificate
• not_nonnegative_incompatibility_of_potential → FiniteInequality.sum_mul_base_nonpos_of_potential
• MaxAffineTransport.exists_isLaxSection_iff_no_nonnegative_certificate → exists_isLaxSection_iff_no_farkasCertificate'
• exists_sparse_farkas_certificate (and rational, integral forms) → exists_sparse_farkasCertificate, …

Graph and transport

• IsStronglyConnectedAt G base → EdgeGraph.IsStronglyConnected G (base-free, mathlib's body)
• Transport.IsSectionWithBase → Transport.IsRootedSection, with its lemmas
• Transport.IsResidualFor → Transport.IsLowerAdjointFor; translationResidual → AdditiveTransport.translationLowerAdjoint
• Graph-sense circuit → cycle in AdditiveTransport: circuitCoefficient, signedCircuitVector, IsGenuineSignedCircuit, exists_simpleSignedCircuit_decomposition → cycleCoefficient, signedCycleVector, IsGenuineSignedCycle, exists_simpleSignedCycle_decomposition. Circuit is kept for the matroid sense, as in IsPositiveCircuit.
• laxified → laxification: laxifiedWeight, laxifiedTranslationTransport → laxificationWeight, laxificationTranslationTransport

Max-affine and recursion

• MaxAffineTransport.holonomyApply → walkApply
• Label.HasCyclicSlack → Label.IsCyclicRelaxationLevel; cyclicSlackThreshold → cyclicRelaxationThreshold; IsSlackChain → IsRelaxedChain
• suffixWeight, suffixWeightSum → suffixSlope, suffixSlopeSum
• TransferSummary.transport, pastTransport → retentionProd, pastRetentionProd
• Arguments named bias and gain in RadiusFixedPoint and ContractiveGauge are now shift and slope, as in the label structure; this affects callers that pass them by name.

v4.34.0

v4.34.0

v4.33.1

v4.33.1