MATH.Preface:9 - Source use and currentness

For formation and composition, Fong and Spivak’s Seven Sketches in Compositionality, §3.2, supplies paths and imposed equations. The patterns adapt these constructions to explicit enabling states and interpretation of composite operations. Direct enumeration remains useful when a small set of paths already answers the question.

For specifying an object through its needed maps, Riehl’s Category Theory in Context, §§2.3, 3.1–3.2, supplies universal properties and set constructions. Fong and Spivak’s Example 3.72 supplies currying: a function with two inputs becomes a function returning a function. MATH.16 uses these constructions to clarify an undecided use; directly defining a familiar representation remains sufficient when that choice is already settled.

Burris and Sankappanavar’s A Course in Universal Algebra, Chapter II, supplies congruences, quotients, term evaluation and isomorphisms. These support MATH.2, MATH.5 and MATH.7. The partial-operation convention in MATH.2 additionally preserves whether an operation is available at the represented state; the total-algebra definition alone does not choose that convention.

For obtaining objects from arguments, Wadler’s Propositions as Types and Rijke’s Introduction to Homotopy Type Theory supply constructive rules and their mathematical setting. The maintained Lean and Rocq accounts linked in MATH.4 and MATH.12 expose the consequences of data representation, proof erasure and choice for execution. The resulting method asks which operation actually obtains the data and permits classical reasoning in a justification of an independently computable operation.

Riehl’s Category Theory in Context, §§1.1, 1.3 and 1.5, supplies composition, transformations preserving it, and equivalence through compatible isomorphisms. MATH.17 uses those structures where the requested operation needs their laws; MATH.18 combines the family-level comparison with direct interpretations of primitives and assertions. A supplied inverse map remains sufficient for a simpler representation question.

For building and changing arguments, the maintained Logic and Proof and Theorem Proving in Lean accounts provide forward and backward proof steps. MATH.19 adapts them to finding a sufficient intermediate claim, including useful generalization; a known direct theorem remains cheaper when it already closes the goal. MATH.22 combines this proof-dependency work with model and interpretation comparison, retaining the distinction between failure of one proof and failure of the theorem.

For bounds and approximations, MATH.20 derives bounds from feasible constructions, universal inequalities and residual-to-error relations, using Vandenberghe’s duality account and Higham’s sensitivity analysis. MATH.21 uses Cauchy completion, compatible finite information and operation-specific convergence. Its maintained Lean sources make the conditions for passing a limit through an operation explicit; Bauer and Kavkler’s constructive-real account supplies an implementation alternative to a fixed convergence rate. The mathematical existence argument and the method of obtaining a requested approximation remain separately available.

For developing a new question, MATH.23 combines Lakatos’s proof-and-refutation method with Georgiev, Gómez-Serrano, Tao and Wagner’s account of AI-assisted conjecture and counterexample work. The latter contributes concrete search and proof routes and their resource limits. The Mathematical Research in the Age of AI declaration raises the retention of mathematical methods as a concern; it is treated as a position in that comparison. The adopted method returns a revised claim and an attainable next operation. A person or an AI agent can supply that contribution.

The symmetry bodies compare group-action constructions with equivariant output requirements and their obstructions. MATH.9’s source account distinguishes compatible selection from the additional regularity questions studied in geometric learning. MATH.10 and MATH.13 retain the separate assumptions for variation, physical conservation and numerical evolution. Return to their source comparisons when one of those stronger conclusions matters.

For invariants, Bayarmagnai, Mohammadi and Prébet supplies a constructive comparison with polynomial-loop methods. MATH.11 uses unknown coefficients and preservation equations at their stated scope. A global polynomial identity is one useful result; a restricted-state question can call for a different construction. The finite-state countercase shows when a cheaper check is sufficient.

These sources play different roles. Established mathematics supplies definitions and arguments; maintained formal libraries and current research expose further constructions, limits and implementation choices. A publication date alone does not make one answer replace another. Revisit a choice when the receiving question changes, a relied-on assumption fails, or another method obtains a more useful result at acceptable cost. The individual bodies keep the operative source passages and the conditions of that comparison.