Part C - Change a construction and develop its theory

MATH.11 - Construct an Invariant from Transformation Rules

Type: Method pattern Status: Stable Normativity: Normative unless marked informative

MATH.11:1 - Problem frame

Use this pattern when a mathematical construction can take many steps and you need a relation that survives every allowed step. Such a relation can rule out a proposed result, constrain a search or derive a formula for a quantity that the steps accumulate.

Here an invariant is a function whose value is unchanged by each allowed transformation. The method constructs that function from the transformations. It starts with a small family of expressions, derives conditions on their coefficients and uses the resulting expression in a proof. Conserved weighted totals, polynomial relations and residues provide different ways to carry out that construction.

First useful move: write one allowed change, substitute it into a candidate expression and calculate what changes. Derive coefficient conditions that make the change vanish, then include the remaining allowed rules. Once preservation holds for them all, compare the invariant at the starting and proposed states.

The reader needs substitution, elementary algebra and the arithmetic used by the example. The polynomial branch uses collection of like terms and linear equations; the residue branch explains arithmetic modulo two. An available invariant can be used directly after checking that it fits the allowed transformations. When a short explicit sequence already answers the question, constructing an invariant may add no useful result.

MATH.11:2 - Problem

Trying more sequences can leave a reachability question unresolved. A proposed formula may hold in the first few calculations but fail at a later step or a different branch. Guessing that an unweighted total stays constant can also fail when a rule replaces two units of one kind with three of another.

The difficulty is to obtain a relation from the actual rules and explain why it survives sequences of arbitrary finite length. A useful relation must then answer the question: a constant function is always preserved, but cannot distinguish a reachable proposal from an impossible one.

The result is a constructed invariant with its preservation argument and a consequence for the stated task. A failed search within the chosen expression family can instead identify a reason to change that family or try another method.

MATH.11:3 - Forces

MATH.11:4 - Solution

Specify the transformations → choose expressions → derive preservation equations → solve and verify → use the invariant → revise the affected part.

MATH.11:4.1 - Specify the states, steps and requested consequence

Let X be the mathematical state set, and write x → y when one allowed step takes x to y. Retain every condition that enables a step and every component of the state that its calculation uses. A rule may be given as y=T(x) with a condition on x, or as a relation allowing several possible successors.

Name the initial state a and the target question. You may need to exclude a particular state b, derive the value of an accumulated quantity after a stated number of steps, or restrict the candidates worth searching.

For an invariant I, the required preservation statement is:

x → y implies I(y)=I(x).

It concerns each allowed step. When several rules or branches are available, each needs that equality. If X describes an external process, establish the correspondence between the mathematical steps and that process through C.29.

MATH.11:4.2 - Choose a small expression family

Look at what the transformations add, remove or combine. For states represented by counts x1,…,xn, try a weighted total:

I(x)=w1*x1+...+wn*xn.

The unknown weights let different kinds contribute differently. For additive changes x → x+d, the change in that total is w1*d1+...+wn*dn.

If the update combines variables or changes an accumulated sum, try a few expressions suggested by those operations. For example, an update containing n can make n² useful because (n+1)^2-n^2=2*n+1. Write a candidate as I(x)=c1*p1(x)+...+ck*pk(x), where the expressions pi are chosen and the coefficients ci are unknown.

A known invariant, a calculated short sequence or an equation needed at the target can suggest these expressions. Choose only as large a family as the next question warrants. A larger polynomial degree adds unknowns and substitution work.

Choose the value arithmetic too. If the question concerns a remainder, calculate the proposed invariant modulo the relevant integer. That can preserve a distinction which an ordinary rational-valued linear expression misses.

MATH.11:4.3 - Derive and solve the preservation equations

For every rule T, calculate I(T(x))-I(x) in the chosen arithmetic. Require it to be zero wherever that step is allowed.

For a rule given as a relation, use I(y)-I(x) on its allowed pairs. A finite relation supplies one equation per pair; a supplied parameterization gives expressions to substitute. If neither is available, obtaining a usable description of those pairs is the missing construction.

For additive count changes, this gives one linear equation on the weights per change. Solve the equations jointly. If all weights must be zero, this family supplies no distinguishing weighted total.

For polynomial updates and a rational-coefficient polynomial family, expand the difference and collect like monomials. Setting every resulting coefficient to zero gives a linear system in the unknown ci. Solving it constructs polynomial identities that preserve I for every input. On a state set or enabled region smaller than the full polynomial domain, this identity test is sufficient but can be stronger than the preservation actually required. A relation valid only on the reachable states may therefore need another construction.

For example, let X={0,1}, T(x)=x² and I(x)=c*x+d. Requiring the polynomial identity c*(x²-x)=0 over all rational x forces c=0. On X the two allowed pairs are 0→0 and 1→1; checking them admits I(x)=x. Starting at 0, this invariant excludes 1. Here inspecting the allowed pairs produces a useful invariant within the same linear family.

The simultaneous equations can be solved by substitution in a small case or by linear algebra for a larger one. If several independent solutions are useful, keep them together as a tuple of invariants. A constant solution can be discarded for a target-separation question because it has the same value at every state.

If a tool proposes coefficients, substitute the resulting expression into the original rules. This confirms the identity and the arithmetic to which it applies. A few numerical trials can reveal an error; a proof for all allowed steps needs the corresponding algebraic argument or an exhaustive finite check.

MATH.11:4.4 - Prove the consequence for a sequence

Let a=x0 → x1 → … → xm be any finite allowed sequence. Preservation gives:

I(xm)=I(xm-1)=...=I(x0)=I(a).

Equivalently, use induction on the number of steps: the zero-step state has value I(a), and one more preserving step keeps that value.

Now use the relation. If I(b)≠I(a), no finite allowed sequence reaches b. If an invariant equation determines an output quantity from other known quantities, derive that output under the equation’s conditions. When several invariants are retained, every component must agree.

For a set of initial states, compare the target’s invariant value with the values of I on that set.

MATH.11:4.5 - Resolve what equality leaves open

If the target and start have the same invariant value, the invariant has supplied a necessary condition. To claim reachability, construct an allowed sequence or use a theorem that supplies one under the remaining conditions.

Inspect a failed continuation. A rule may be irreversible, lack the required input units or require an order the invariant ignores. Refine the state or expression when that can answer the question. MATH.1 constructs paths with their intermediate conditions; MATH.8 generates a family when the available transformations form the relevant symmetry action.

When the coefficient calculation yields only constants, state the family actually exhausted. Changing from linear to polynomial expressions or from rational values to residues can change what is found. General polynomial-invariant search has its own algorithms and scope conditions; it is worthwhile when the simpler construction leaves a consequential question open.

Stop with the established formula, impossibility result, useful restriction or identified next construction. A request for one of these results need not expand into finding every invariant.

MATH.11:4.6 - Retain the construction through a change

For a changed initial state, retain the preservation equations and recompute the initial invariant value. For a changed target, compare its value using the same proved relation.

For an added or altered transformation, substitute that rule into the current invariant first. If it fails, include the new preservation equation and solve the affected system again. Removing transformations preserves any old invariant, although further invariants may become available.

A change of arithmetic, rounding or retained state can change the algebra itself. Recompute the affected identity before using its consequence. MATH.7 can transport the expression through a reversible representation; MATH.2 addresses an identification that must preserve a requested operation or answer. B.5.RR follows the changed mathematical result through a larger argument.

MATH.11:5 - Archetypal Grounding

MATH.11:5.1 - Derive weights for an exchange construction

States are triples (a,b,c) of nonnegative integer counts. Two rules are allowed:

• Replace two A units with three B units when a≥2: (a,b,c) → (a-2,b+3,c).
• Replace one B unit with one C unit when b≥1: (a,b,c) → (a,b-1,c+1).

Starting with four A units, can the construction end with exactly five C units and nothing else?

The unweighted count changes under the first rule. Try I(a,b,c)=α*a+β*b+γ*c. The two differences are -2*α+3*β and -β+γ. Their joint equations have the solution (α,β,γ)=(3,2,2), giving:

I(a,b,c)=3*a+2*b+2*c.

Every allowed step preserves this value. The start (4,0,0) has value 12; the target (0,0,5) has value 10. The target is impossible under the stated rules, however many steps are attempted.

The same invariant helps formulate a useful alternative: six C units have value 12. They are attainable. Apply the first rule twice to obtain (0,6,0), then the second rule six times to obtain (0,0,6). This sequence supplies the contribution that equality of the invariant alone left open.

Now start at (0,3,0) and ask for (2,0,0). Both values are 6, but the first rule cannot create A and the second only consumes B to create C. Thus the requested target is unreachable. Adding the reverse exchange (a,b,c) → (a+2,b-3,c) when b≥3 makes that target reachable in one step. Its invariant change is 2*3-3*2=0, so the old invariant survives while the reachability answer changes.

For a material or operational application, interpret the counted kinds and allowed exchanges before using this mathematical result. The calculated weights express preservation by these rules; identifying them with physical mass or monetary value requires the corresponding subject account.

MATH.11:5.2 - Derive an accumulated sum from an update

A construction starts at (n,s)=(0,0) and repeatedly applies:

(n,s) → (n+1,s+n+1).

The question is what s will be when n has reached a chosen nonnegative integer. The new term added to s depends on n, so try I(n,s)=a*s+b*n^2+c*n+d.

Substitution gives:

I(n+1,s+n+1)-I(n,s)=(a+2*b)*n+(a+b+c).

Set a+2*b=0 and a+b+c=0. Choose a=2, b=-1, c=-1 and d=0. The resulting invariant is I(n,s)=2*s-n^2-n. It starts at zero, so every state reached by the update satisfies:

2*s=n^2+n, hence s=n*(n+1)/2.

After three steps, (3,6) satisfies it. The proposed state (3,7) has invariant value 2 and cannot result from these updates.

The same relation can be used with a different start. Starting at (2,10) gives invariant value 14, so later states satisfy 2*s-n^2-n=14. One step produces (3,13), which satisfies that changed equation. The preservation proof is unchanged.

Now change the update to (n,s) → (n+1,s+2*n+1). Substitution into the old invariant gives change 2*n, so the old formula fails in general. Reusing the same candidate family gives equations 2*a+2*b=0 and a+b+c=0. Choose a=1, b=-1, c=0: the new invariant is s-n^2. From (0,0), it gives s=n^2.

These constructions use integer arithmetic without overflow. They also use the update as a simultaneous substitution: the expression for the new s contains the old n. An implementation that increments n before evaluating that expression would need a different calculation.

MATH.11:5.3 - Change the value arithmetic to find a parity obstruction

The state is an integer n. Allowed steps add 2 or subtract 2. Starting at zero, can the construction reach 1?

A rational-valued linear candidate I(n)=a*n+b changes by 2*a under addition of 2. Requiring zero forces a=0, leaving only constants in this family.

Instead take I(n)=n mod 2, with values 0 and 1. Both +2 and -2 preserve the remainder. The start has remainder 0 and the target remainder 1, proving impossibility.

Here the necessary condition also leads to a construction. For any even target n=2k, use k additions of 2 when k≥0, or -k subtractions of 2 when k<0. Thus the reachable states are exactly the even integers. The invariant and the explicit sequence establish the two directions of that statement.

Adding the steps +1 and -1 destroys this parity invariant: 0 can now move to 1. Every integer becomes reachable by repeated unit steps. The earlier two-step rules and their parity calculation remain correct, but no longer cover all allowed steps.

MATH.11:6 - Bias-Annotation

A familiar conserved total can be imposed before examining the transformations. Deriving its weights from each rule makes the assumed conservation testable. A small search can also encourage the claim that no useful invariant exists; retain the searched expression family and arithmetic when interpreting its failure.

An easily generated invariant may have little value for the target question. Compare its values or use its equation to obtain a consequence before investing in a larger repertoire.

MATH.11:7 - Conformance Checklist

For the construction and use at hand:

1. The state set, initial condition and every allowed transformation are recoverable.
2. The candidate expression family and its value arithmetic are stated.
3. The preservation equations cover all allowed rules, with any stronger polynomial-identity requirement visible.
4. The constructed expression satisfies those equations and gives the stated initial value.
5. The finite-sequence argument supplies the reach of the conclusion.
6. An impossibility claim separates invariant values; a reachability claim also has its sequence or sufficient theorem.
7. A failed invariant search retains the family and scope actually searched.
8. Changes to initial data, target, transformations or arithmetic reopen the corresponding calculation.

Recognition can begin with one rule and a useful candidate expression. Assurance of a general consequence examines the preservation and sequence argument on which that consequence depends.

MATH.11:8 - Common Anti-Patterns and How to Avoid Them

MATH.11:9 - Consequences

A small equation system can replace an unbounded search for an impossible construction. The resulting relation can also derive an output formula or narrow the next construction to candidates consistent with it.

The method’s cost depends on the chosen expressions and substitutions. Weighted totals are often inexpensive; polynomial expansion can grow quickly. When an invariant leaves the consequential question open, a constructive path or a different mathematical method may be the better next move.

MATH.11:10 - Architectural Rationale

The preservation question is local to a transformation, while the useful conclusion concerns any finite composition of transformations. The sequence argument joins those scales. Deriving the expression from the rules supplies the missing step in the advice to “find an invariant.”

Unknown coefficients turn a family of guesses into equations. Weighted counts expose exchange ratios; polynomial terms expose accumulation; residues retain divisibility information. The examples use different arithmetic but the same question: what function stays unchanged, and what does that prevent or determine?

An invariant usually compresses the state. Equality of its values can forget irreversible directions or unavailable inputs, as the exchange example shows. A proof of reachability therefore needs more than this compression. Conversely, different values can close an impossibility question without reconstructing every sequence.

These are mathematical constructions even when their states represent programs, resource transformations or physical models. Their interpretation and use in another subject need the correspondence and premises of that subject. Mathematical construction, subject interpretation and implementation can be divided among contributors while preserving those dependencies.

MATH.11:11 - SoTA-Echoing

For deriving a condition valid after arbitrarily many steps, adopt the induction-based Invariant Principle in Lehman, Leighton and Meyer’s Mathematics for Computer Science, §5.4.3. Compared with inspecting more executions, :4.4 uses one preservation proof to cover every finite sequence. This pattern constructs an invariant function; the book’s principle also covers broader preserved predicates. Stop when the resulting relation answers the question, and reopen if an allowed transition changes. MIT text.

For constructing polynomial expressions from update rules, adapt Bayarmagnai, Mohammadi and Prébet’s Algebraic and Algorithmic Methods for Computing Polynomial Loop Invariants, §5, Corollary 5.4 and Algorithm 6. The adopted move substitutes an expression with unknown coefficients and solves the resulting linear equations. It improves on unstructured guessing in :4.2-:4.3 and the sum construction in :5.2. The source’s stronger algorithms distinguish invariant form, initial-value conditions and search space. Here the polynomial-identity construction has its stated scope; a restricted reachable-set question can require a different method. Reopen when a richer family or specialized algorithm obtains a more useful relation at acceptable cost. Extended paper.

For count transformations, adapt the conserved linear expression described by Gopalkrishnan in Autocatalysis in Reaction Networks. The weighted-exchange derivation in :5.1 makes such a quantity available instead of assuming an unweighted total. Equal values still require a reachability construction. The source’s chemical-network results need their own premises; they are not used to identify the counted kinds in this mathematical example. A changed exchange rule reopens the weight equations. Author’s account.

The three worked constructions and their changed conditions are derived here. The source algorithms do not establish that these mathematical rules describe a particular physical system or implementation.

MATH.11:12 - Relations

• MATH.1 constructs permitted paths and retains intermediate state; MATH.4 constructs witnesses by induction. This pattern constructs a preserved function and uses induction to obtain its consequence.
• MATH.2 forms identifications under retained operations. Equal invariant values give a possible identification, whose adequacy for another operation remains a separate question.
• MATH.5 extends a supplied generator assignment through composites. This method instead solves for an assignment that transformations preserve.
• MATH.7 transports an expression with its structure through a bijection. MATH.8 generates solution orbits; an invariant can rule out membership but need not distinguish all orbits.
• B.5.RA recovers the resulting argument; B.5.RR revises its affected dependencies; B.5.QD develops the next question from its obstruction or formula.
• C.29 connects the mathematical result to another subject. C.11.DUA helps decide whether a larger invariant search would change the next useful action.

MATH.11:End

MATH.13 - Derive a Consequence from a Symmetry

Type: Method Status: Stable Normativity: Normative

MATH.13:1 - Problem frame

Use this pattern when a transformation appears to preserve the structure relevant to a problem, and you need to turn that observation into a useful restriction, a transferred solution or a reason that a requested answer cannot be selected from the available information.

A symmetric allocation problem can constrain its unique optimum before a full calculation. An anonymous arrangement can make a unique choice impossible under a stated selection rule. A rotationally symmetric physical law can relate motions with different initial states. The useful consequence depends on what the transformation actually preserves and how the required answer transforms.

A symmetry here is an invertible transformation preserving the stated structure. The object of the Method is that transformation together with the problem and answer it acts on. State the structure: preserving a shape, an equation, a criterion or a fully specified problem gives different premises.

The first result is a consequence with its reason: another valid solution, a restriction on possible answers, or a conflict between the input symmetry and the required output. This can reduce a search or identify the additional distinction a computation needs.

The reader needs the problem’s conditions and enough subject mathematics to apply the transformation and test its effect. The allocation and selection examples need algebra and permutations. The dynamics example additionally needs differentiation and elementary state updates.

If no symmetry-related conclusion is needed, use the direct calculation. If the live problem is a general change of mathematical representation, C.29.1 supplies result transfer without requiring a symmetry.

MATH.13:2 - Problem

A suggestive symmetry can omit the feature that decides the problem. Equal-looking components can have different costs. A law can be unchanged while its boundary or initial data change. A function can require its output to rotate with its input rather than stay numerically identical.

A second error begins after a real symmetry is established: the solver assumes more than it implies. A symmetric problem can have several asymmetric solutions. A rotation-respecting numerical scheme can fail to conserve the physical angular momentum. To obtain a usable conclusion, follow the transformation through the actual solution condition.

MATH.13:3 - Forces

MATH.13:4 - Solution

Specify the transformation → follow every relevant condition → transform the answer → derive the consequence → use it within those premises.

MATH.13:4.1 - Name what must stay the same and what may transform

Recover the problem: admitted candidates, supplied data, conditions, criterion if there is one, and the required kind of answer.

Choose a transformation g and say how it acts on those participants. A permutation can exchange components; a rotation can change coordinates or rotate a physical configuration. Explain which operation is intended. For a symmetry claim, the transformation must be invertible on the relevant domain and retain the stated structure.

Several transformations may form a group: they include doing nothing, composing transformations and undoing each transformation. Name the action on the objects used by the problem. A familiar group name alone leaves that action unspecified.

Keep supplied data in the comparison. If swapping two components also swaps their different costs, the result can be an equivalent problem with transformed data. It is a symmetry of the fixed original problem only if the data required to remain fixed are preserved.

MATH.13:4.2 - Establish the problem-to-solution relation

Apply the transformation to the conditions. Show that an admitted solution is taken to an admitted solution of the stated target problem.

For an optimization problem, check feasibility and the criterion. If g maps the feasible set onto itself and J(g(x))=J(x), it maps every minimizer to a minimizer of that same problem.

For a rule f:X->Y, specify the input action g and the corresponding output action r(g). The relation

f(g(x))=r(g)(f(x))

is called equivariance: transforming the input and then computing agrees with computing and then transforming the output. Invariance is the case where the output stays unchanged. Classification of an object and prediction of its position can require these different relations.

For a dynamics law, transform the state, parameters and initial or boundary data. A transformed trajectory may solve the law with transformed data. Establish that correspondence before claiming anything about the solution with the original fixed data.

Use a mathematical argument for the range claimed. A few successful transformations can reveal or test a candidate symmetry; a conclusion covering an entire stated family requires the corresponding preservation argument.

MATH.13:4.3 - Obtain the useful consequence

Follow the consequence needed by the question.

Transfer a solution. From a known solution x, obtain g(x) and use the preservation argument from :4.2 to establish what problem it solves. Compositions can generate further related solutions. These are distinct answers only when the transformed objects differ under the problem’s equality.

Restrict a unique solution. If the fixed problem has exactly one solution x, every symmetry g of that problem must satisfy g(x)=x: g(x) is a solution, so uniqueness identifies it with x. Solve this fixed-point condition to restrict or find the candidate.

If uniqueness has not been established, retain the weaker result: symmetries move solutions within the solution set. A symmetric candidate may be worth testing, but the existence of asymmetric solutions remains possible.

Test a requested deterministic answer. Suppose an input x is fixed by g and the requested rule must be equivariant. Then f(x)=r(g)(f(x)). Check whether any permitted output can satisfy that condition for every transformation fixing x. If none can, the requested deterministic rule cannot answer that input under the stated requirements. The missing distinction or incompatible output requirement is a useful result.

These deductions use preservation and, where stated, uniqueness or equivariance. A conservation law along physical time evolution is a different conclusion. Obtain it from the dynamics or the applicable theorem, including its conditions.

MATH.13:4.4 - Preserve the information needed for use

When symmetry reduces a calculation, state what the reduced answer means in the original problem.

An invariant output can often be calculated from a representative of a symmetry class. An equivariant output may need the transformation used to choose that representative so the answer can be returned to the original coordinates. If several transformations give the same representative, their different output actions must agree on the returned answer, or the result remains ambiguous.

For example, rotating an image to a standard orientation can help classify the object. Reporting a location in the original image additionally requires the corresponding inverse coordinate transformation. If the task distinguishes orientations, the normalization must retain that information.

Use C.29.1 when establishing this representation-and-return relation is itself the difficulty. Use C.29.2 to construct the actual computation; the existence of a symmetric formulation does not supply an efficient algorithm.

MATH.13:4.5 - Return a failed symmetry to its decisive premise

When the comparison in :4.2 fails, identify what changed: an allowed candidate, supplied datum, criterion, output meaning or modeled law. Use that difference to revise the symmetry claim or the problem formulation.

An approximate symmetry can still help, but the allowed discrepancy must be related to the requested result. Establish the bound needed by that use. Small-looking changes are insufficient when they reverse a selection or destroy uniqueness.

After obtaining the consequence, continue with the reduced calculation, transferred solution or revised requirement. Stop when it answers the current question. Add observations or input distinctions only when they can resolve the remaining choice; C.11.DUA supplies the cost-sensitive decision about further work.

MATH.13:5 - Archetypal Grounding

MATH.13:5.1 - A symmetric allocation and an asymmetric optimum

Let x1,x2>=0, x1+x2=10, and minimize J=x1^2+x2^2. Swapping x1 and x2 preserves both the feasible set and J.

The cost is strictly convex on this feasible segment, and a minimizer exists because the segment is compact and the cost is continuous. Hence the minimizer is unique. The symmetry condition requires (x1,x2)=(x2,x1), so the only possible optimum is (5,5). The direct calculation J(5+h,5-h)=50+2*h^2 confirms it for every feasible h.

Now use J=x1^2+2*x2^2 under the same resource constraint. Swapping the allocations changes the cost: J(10,0)=100 and J(0,10)=200. The original exchange symmetry is gone. The optimum is (20/3,10/3), as the admissible-variation construction in MATH.10 shows.

Symmetry alone also need not make individual solutions symmetric. If the original sum-of-squares criterion is maximized on the same segment, (10,0) and (0,10) are both maxima. The swap exchanges them. The midpoint is fixed by the swap but is the minimum, so selecting it from symmetry without the uniqueness and optimization premises would answer a different question.

MATH.13:5.2 - A unique choice from an indistinguishable arrangement

A selector receives a three-vertex cycle with identical vertex attributes and equal edge attributes. Its output must designate exactly one vertex. Rotating the cycle is treated as a relabeling: the requested deterministic rule must rotate its selected vertex in the same way.

For this input, a one-step rotation leaves the supplied arrangement unchanged. Equivariance therefore requires the selected vertex to be fixed by that rotation. No vertex is fixed: each moves to the next vertex. The requested deterministic selector has no permitted output for this input.

One repair is to supply a distinguished attribute, such as an available unique priority, and let the rule use it. Another is to change the requested result to the set of all three equally admissible vertices. Random selection is another problem: a uniform distribution can be rotation-invariant even though a sampled vertex is not fixed. The construction of a coordinated random choice would need its own procedure.

This is a mathematical result about the given input and rule requirements. Extra identifiers, timing distinctions or other available attributes can change the input symmetry and therefore the conclusion. It does not establish that every real three-agent arrangement faces this obstruction.

MATH.13:5.3 - A symmetry of motion and what a numerical step preserves

Consider the planar model qdot=v, vdot=-q. Applying the same planar rotation R to q and v preserves these equations. Thus a trajectory starting at (q0,v0) produces a rotated trajectory starting at (R*q0,R*v0).

For q0=(1,0), v0=(0,1), a quarter-turn changes the initial data. The transformed trajectory solves another initial-value problem. Uniqueness for the original data therefore does not imply that its trajectory is fixed by every rotation.

In this model, J=x*vy-y*vx is angular momentum for unit mass. Direct differentiation gives

Jdot = x*ay-y*ax = x*(-y)-y*(-x)=0.

This establishes conservation along its trajectories. A radial law vdot=-k(t)*q gives the same cancellation. The proof uses the acceleration relation; the rotational description alone is not the argument.

Now compute with explicit Euler:

q_next=q+h*v; v_next=v-h*q.

The update is equivariant under the same rotations because R distributes over the linear combinations. Yet substitution gives

J_next=(1+h^2)*J.

Starting with J=1, h=0.1 and taking one hundred steps yields about 2.7048. Rotation equivariance of the scheme has survived while conservation of J has failed. If the question uses angular momentum, the computational construction must be changed or its error made acceptable for that use.

For this model, the update v_next=v-h*q; q_next=q+h*v_next preserves J by substitution. Its preservation of this quantity is one property of that scheme; questions about phase or other errors retain their own numerical analysis.

MATH.13:6 - Bias-Annotation

Visual sameness can distract from a cost, label meaning or boundary datum that distinguishes the cases. Transform those inputs explicitly.

A solver familiar with unique linear problems may carry uniqueness into a problem with several solutions. Keep the solution-set result available until uniqueness has its own basis.

A conserved-looking scalar can also invite the wrong inference from equivariance. Distinguish a quantity unchanged under a spatial transformation from a quantity unchanged as the system evolves. The oscillator computation exposes the practical difference.

MATH.13:7 - Conformance Checklist

MATH.13:8 - Common Anti-Patterns and How to Avoid Them

MATH.13:9 - Consequences

Symmetry can reduce calculation, generate useful related solutions or expose an impossible selection requirement before implementing a solver. The preservation argument also locates what new information would make a choice possible.

The main cost is identifying the relevant structure and following the transformation through the whole problem. Large or continuous symmetry groups may require substantial mathematical methods. The direct consequence obtained here can make that further work worthwhile or show that the simpler calculation already suffices.

MATH.13:10 - Architectural Rationale

The Method follows a transformation through a problem and its answer. This keeps a visible symmetry from becoming an unrestricted claim about every quantity or every use.

The fixed-point argument is particularly useful because it converts invariance of the input into a restriction on the answer. Uniqueness and equivariance enter at the point where that conversion needs them. Keeping those premises explicit makes the same reasoning useful in optimization, mathematical construction and computational selection.

A dynamics symmetry, a conservation theorem and a numerical method can contribute to one physical answer while doing different work. The oscillator case retains that connection and exposes where a valid property is lost during computation. A specialized construction of Noether quantities or structure-preserving integrators is a further Method when that result is required.

MATH.13:11 - SoTA-Echoing

The selected approach defines the structure and input-output action before using symmetry. It supports direct algebra for a small problem and provides the premise for more specialized group, optimization or numerical constructions.

Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning, draft chapter 3, §§3.1-3.2 develops symmetries as invertible structure-preserving maps and distinguishes invariant and equivariant outputs. Adopt that explicit action and output discipline. Whether a transformation preserves a label or target still comes from the modeled task. Architecture construction and learning-performance claims need the corresponding further Methods and evidence.

Tong, Classical Dynamics, §2.4 derives conserved quantities from continuous symmetries of a Lagrangian using its equations of motion. The useful contribution is the extra argument connecting symmetry with time evolution. The simple oscillator calculation above performs that connection directly; it does not substitute for the wider Noether construction.

Hairer, Geometric Numerical Integration, lecture 2, §1 supplies the symplectic Euler formulas and their Hamiltonian conditions. The direct comparison above shows why a requested invariant must be examined under the actual numerical update. A different model or requested accuracy can favor a different scheme.

C.29.1 supplies the general result-transfer comparison. The fixed-point and selection constructions here make one specific consequence available without a full group-theory survey. Revisit the use when its structure, output meaning, uniqueness premise or transformation law changes.

MATH.13:12 - Relations

• C.29 establishes the mathematical interpretation and its return to the working subject.
• C.29.1 constructs the preservation and recovery of a result through a changed representation.
• MATH.10 derives consequences from changes that retain constraints; symmetry additionally preserves the specified structure or criterion.
• C.29.2 and C.29.3 connect a computation with its represented operations and realization.
• A.3.3.TR constructs state change from the available laws. B.5.MPC connects that physical account with mathematical and computational contributions.
• B.5.RR revises reasoning after a premise changes. C.39 helps obtain a missing construction or reformulate an obstructed result.

MATH.13:End

MATH.8 - Generate a Solution Family by Symmetry

Type: Method Status: Stable Normativity: Normative

MATH.8:1 - Problem frame

Use this pattern when a mathematical solution is known and transformations that preserve its defining conditions can produce further useful solutions. You may need related roots of an equation, arrangements considered equivalent under rotation, or answers to problems whose data have been permuted.

Start with the known solution and one proposed transformation. Apply it and establish which problem the result solves. This can return another answer immediately, expose changed data, or identify a condition that the transformation fails to preserve.

A symmetry is an invertible transformation preserving the structure named by the problem. Its orbit at an object is the family of objects reached by the chosen group of transformations. The construction below obtains that family, distinguishes repeated objects, and explains what is still missing from a claim to have found all solutions.

The reader needs sets, functions, elementary equations and composition. The required group-action rules are stated below. The polynomial example uses factorization; the finite-arrangement example needs only binary strings and rotation. Use a direct calculation when it already supplies the needed answer. A transformation that changes the problem can still transfer a solution to the changed problem when that is useful.

MATH.8:2 - Problem

Several transformed answers can be repetitions of one object. An orbit can also omit whole families of solutions. Conversely, a supposed symmetry can change a coefficient or boundary datum that the original problem holds fixed.

The mathematical task is to obtain solutions with a stated reach. This requires the transformation’s action on both data and candidate answers, an argument that it preserves the solution condition, and a way to identify the objects its repeated use actually reaches.

MATH.8:3 - Forces

MATH.8:4 - Solution

Specify the actions → preserve the solution relation → transform a known solution → construct its orbit → establish the family’s reach → return the needed answer.

MATH.8:4.1 - Specify the problem and the transformations

Write the solution condition as S(d,x): candidate x solves the problem with data d. State the data that are held fixed, the domain of candidates and the equality used to distinguish answers. An equation, a feasibility condition or a minimum under a stated criterion can provide S.

Give the transformations and their actions on d and x. For a group G, the action satisfies e*x=x and (g*h)*x=g*(h*x); the same rules apply to the data action. Here e is the identity transformation, and multiplication in G means composition, with h applied first. Every g has an inverse. A supplied family of permutations can make these rules immediate.

If the group is given by generating transformations, include their inverses and retain the relations they must satisfy. MATH.5 can construct an action from generator images that respect those relations. Listing generators without their action leaves the proposed symmetry undecided.

For a fixed datum d, retain only transformations with g*d=d. These form its stabilizer: the subgroup of transformations that leave that datum unchanged. Include compositions when finding this subgroup: the two-mark case in :5.2 is fixed by a half-turn although a single turn changes the marks. A larger group can relate different data instances, which is a different useful calculation.

MATH.8:4.2 - Establish the solution-preserving relation

Show that S(d,x) implies S(g*d,g*x) for every transformation and candidate in the claimed range. Applying the same implication to the inverse gives the converse. The transformation therefore pairs the two solution sets.

For an equation, substitute the transformed variables and data. For several constraints, preserve each one used by the solution. An optimization result needs both transformed feasibility and the corresponding criterion: if feasible candidates are paired bijectively and J_(g*d)(g*x)=J_d(x), a better transformed candidate would return a better original candidate. Thus a minimizer transfers.

Preservation for generating transformations and their inverses extends to every finite composition by applying the implications successively. Use MATH.4’s finite-construction argument when that extension needs explanation. A check on a few candidate values establishes only those cases unless a general argument is also available.

If a transformation fails, retain the first changed condition and decide whether the changed problem is useful. MATH.6 can exhibit the failure; FPF C.29 relates the mathematical correspondence to another subject when one is involved.

MATH.8:4.3 - Generate related solutions and remove repetitions

From a known solution x, calculate g*x and return it with the data g*d. To obtain solutions of the original fixed problem, use its data stabilizer from :4.1.

For a chosen group H acting on the same fixed problem, define the orbit:

H*x={h*x | h in H}.

All its members solve that problem by :4.2. Compare the resulting objects using the problem’s equality; distinct transformation expressions can give equal answers.

With a finite list of generating transformations, a finite orbit and decidable equality, generate the orbit by closure. Start with x. Apply each generating transformation and its inverse to every newly found member, adding only previously absent results. Once every stored member has been processed and no new one appears, the set is closed under the generators and inverses. Every finite word in them stays in that set, so it is the whole generated orbit.

This procedure terminates when the reached orbit is finite and the stated operations return. For an infinite orbit, a formula such as {h*x | h in H} with a usable parameterization can be the result. A stopped enumeration without closure supplies only the reached subset.

MATH.8:4.4 - Explain duplicates and the limit of one orbit

The transformations fixing x form its stabilizer H_x={h in H | h*x=x}. Two transformations give the same answer precisely when the composition of one with the other’s inverse fixes x:

h1*x=h2*x exactly when (h2^-1*h1)*x=x.

Choose one transformation h0 in H. All transformations returning the answer h0*x have the form h0*k with k in H_x: composing with k leaves x unchanged, and any h giving that answer satisfies h0^-1*h in H_x. These sets of transformations are called the left cosets of the stabilizer. They partition H, and each contains as many transformations as H_x, since multiplication by h0 is reversible. Therefore, for finite H, the number of distinct answers is |H|/|H_x|. Use this count when it helps construct or check the requested family; explicit comparison can be simpler for a small example.

One orbit contains exactly the answers reachable from its starting member under H. To claim all solutions, establish that every solution belongs to a represented orbit. This can use a complete finite classification, a mathematical reduction, or an argument that H acts transitively on the solution set, meaning that every solution is reachable from the starting solution. Finding no new member in the current orbit proves its closure, not that another orbit is absent.

When another solution lies outside the family, use it as the starting member of another orbit. A property unchanged by every transformation can show that two candidates cannot belong to the same orbit. Such a property can also suggest what a wider transformation group would need to change.

MATH.8:4.5 - Use an orbit representative without losing the requested result

A quantity constant on each orbit can be calculated from any representative. To define additional operations on orbit classes, use MATH.2’s representative-independence condition; an orbit partition by itself only supplies classes.

When a problem is solved using representative data d0 and solution x0, retain a transformation g with g*d0=d for the requested data d. Return g*x0. If two transformations satisfy g1*d0=g2*d0=d, an answer independent of that choice requires g1*x0=g2*x0. A disagreement identifies information that the representative alone does not supply.

MATH.13 supplies the fixed-point restriction on a unique solution and the test for an impossible equivariant choice. Those questions require the output action and, for the unique-solution deduction, a justified uniqueness premise. Generating a solution set here does not select one member from it.

Stop with the requested related solution, complete orbit, orbit classification or identified failure of preservation. When data, constraints or the output change, reopen the affected action and preservation argument before reusing the family. A more costly enumeration or symmetry computation is useful only if it can improve the receiving result.

MATH.8:5 - Archetypal Grounding

MATH.8:5.1 - An even polynomial has more than one solution orbit

For real x, solve P(x)=x^4-5*x^2+4=0. The two transformations are identity and sign reversal r(x)=-x. Since P(-x)=P(x), they preserve the equation.

The known solution 1 gives the orbit {1,-1}. Applying sign reversal again returns to 1, so this orbit is complete. It is not the complete root set: 2 also solves the equation and belongs to the different orbit {2,-2}.

Factorization P(x)=(x^2-1)*(x^2-4) establishes that these two orbits cover all real roots. Symmetry generated each pair; factorization supplied the missing completeness argument.

Now change the equation to Q(x)=x^2+x-2=0. The value 1 remains a root, but Q(-1)=-2. The linear term breaks the sign symmetry. Reusing the old transformation would give a false answer to the changed problem.

MATH.8:5.2 - Binary arrangements on a cycle

Consider binary strings of length four with exactly two entries equal to 1. Positions are numbered 0 through 3 around a cycle. Let r move each entry to the next position, wrapping the last to the first. Four rotations return the original string, and rotation preserves the number of ones.

Starting with 1100, repeated rotation gives:

1100 -> 0110 -> 0011 -> 1001 -> 1100.

There are four distinct members. Only the identity rotation fixes 1100, agreeing with the count 4/1=4.

Starting instead with 1010 gives:

1010 -> 0101 -> 1010.

A rotation by two positions fixes either alternating string. Its stabilizer has two members, so the orbit count is 4/2=2.

Every two-one string either has adjacent ones around the cycle or has opposite ones. This covers the six possible strings and separates the two orbits. If the question asks for arrangements up to rotation, two representatives suffice. If it asks for every labeled string, return all six.

If position 0 receives a distinguished mark that must remain fixed, only the identity rotation preserves that data. The old orbit classification then forgets a distinction required by the new problem. The strings remain available; their identification must change.

Instead put identical marks at positions 0 and 2, with neither mark distinguished from the other. A single rotation and its inverse move the marked set to {1,3}; a half-turn returns it to {0,2}. The data stabilizer is therefore {e,r²}. To find this subgroup, examine compositions such as r² as well as the supplied generators.

MATH.8:5.3 - Permuting coefficients changes which equation was solved

Let the data be coefficients a=(2,1) and right-hand side 5. The equation is 2*x1+x2=5, with known solution x=(1,3).

The swap sends a to (1,2) and x to (3,1). Their scalar product remains 5 because both positions are exchanged. Thus the transformed solution satisfies x1+2*x2=5.

Keeping the original coefficients instead gives 2*3+1=7. The swap preserves the relation between transformed data and transformed solutions; it does not preserve this fixed original equation.

For comparison, x1+x2=5 has equal coefficients. Its data are fixed by the swap, so a solution (1,4) gives another solution (4,1) of the same equation. Neither the swap nor the equation singles out one of them. A requirement for one distinguished answer needs an additional criterion or a compatible choice method.

For a representative-data calculation, take coefficients (1,2) and its solution (3,1). The swap maps those data back to (2,1) and the solution back to (1,3), recovering the original answer. With the equal coefficients (1,1), both identity and swap return the same data, while the chosen solution (1,4) returns as either (1,4) or (4,1). Each is a valid solution, but this choice does not define a transformation-independent rule. This ambiguity concerns the chosen pair; a request for a swap-fixed solution can instead use (5/2,5/2).

MATH.8:6 - Bias-Annotation

Finite permutations make complete orbits cheap to display. Infinite and continuous actions can instead require symbolic parameterizations, different equality procedures or further mathematical methods. The complete finite examples therefore establish their own construction, while the general group argument states what can be reused.

Familiar visual symmetry can also hide supplied labels or coefficients. The equation and marked-cycle cases keep those data in the comparison.

MATH.8:7 - Conformance Checklist

• The actions on the data and candidates satisfy the claimed composition and inverse rules.
• The preservation argument uses every condition required by the solution.
• Each returned solution is attached to its unchanged or transformed data.
• Distinct orbit members are distinguished by the problem’s equality.
• A complete-orbit claim has closure or a corresponding argument; an all-solutions claim covers the other possible orbits too.
• A representative retains the information required to recover the requested answer.

MATH.8:8 - Common Anti-Patterns and How to Avoid Them

Close one orbit and declare the equation solved. The polynomial has two complete sign orbits. Supply the additional classification or restrict the returned claim to the generated family.

Count transformation expressions as different solutions. The alternating string is fixed by a half-turn. Compare objects or use the stabilizer to account for repetition.

Transform variables while silently retaining changed data. Swapping variables and coefficients preserves the linear relation; swapping only the variables can fail it. Return the corresponding data with the solution.

Use every old rotation after a mark is added. The fixed mark changes the permitted subgroup. Recompute the identification from the new data.

Return a normalized answer without its coordinate relation. An invariant quantity and an equivariant answer need different return information. Retain the transformation or expose the remaining ambiguity.

MATH.8:9 - Consequences

A known solution can supply a useful family without solving every transformed case independently. Orbit closure and stabilizers explain both the family and its repetitions. Separate orbits reveal a remaining construction problem rather than an apparent lack of progress in the same enumeration.

The gain depends on the cost of finding and applying the transformations. For a small isolated equation, direct calculation may finish sooner. For repeated or related questions, the shared preservation argument can save substantial work; the construction alone does not quantify that saving.

MATH.8:10 - Architectural Rationale

The method builds a solution family from an action and a preservation relation. Keeping data inside that relation distinguishes transformations of one fixed problem from transformations between problems of the same form.

Generating the orbit and classifying all solutions answer different questions. The finite-closure argument explains when generation is complete; a stabilizer explains repeated results; another representative or reduction accounts for a missing orbit. These operations keep useful mathematical content beyond the instruction to notice a symmetry.

MATH.7 constructs operations through an arbitrary bijection. Here the transformations act on a specified problem and preserve its solution relation. MATH.5 can construct the action from assigned generators, while MATH.2 controls additional operations on identified results. The same orbit can support different receiving questions without giving its quotient every operation of the original set.

A direct solution, an existing orbit classification or a supplied parameterization is preferable when it already supplies the requested result. The group construction earns its cost when related answers, reduced cases or the reach of a family matter.

MATH.8:11 - SoTA-Echoing

Question: how can transformations construct related mathematical solutions while retaining data, distinguishing repetitions and establishing the reach of the family?

Milne’s Group Theory, version 4.01, November 2025, chapter 4, definition 4.1, the orbit discussion and proposition 4.7/corollary 4.8, supplies actions, orbit partition and the stabilizer description of an orbit. Adopt those mathematical relations. The procedure here makes finite generation, returned data and the separate all-solutions question explicit.

Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning, chapter 3, §3.1 distinguishes the structure preserved by an automorphism from a change to an isomorphic object. Adapt that distinction to a relation between problem data and solutions. A fixed mark or coefficient can change the available symmetries.

The selected construction competes with direct calculation or a ready classification. It is useful when one preservation argument replaces repeated solution work or exposes omitted families. Direct calculation remains sufficient for a single easy result. The finite examples demonstrate closure and incomplete coverage; they make no comparative performance claim for a solver or learning system.

Reopen when the action, data, solution relation, equality procedure or requested return changes. A more effective orbit-generation or canonicalization method can replace the finite implementation while retaining its required mathematical result.

MATH.8:12 - Relations

• Uses MATH.1 and MATH.5: compose generating transformations and construct an action that respects their relations.
• Uses MATH.4: extend preservation through finite compositions and justify the finite-closure result.
• Uses MATH.2: decide which further operations remain defined on orbit classes.
• Connects with MATH.6: exhibit a changed condition or a counterexample to a completeness claim.
• Connects with MATH.7: compare an arbitrary representation change with an action preserving a given structure.
• Uses C.29 for another subject: recover what the mathematical transformation and returned solution mean there.
• Uses MATH.13 when the requested answer is unique or must be chosen equivariantly: obtain its fixed-point restriction or an obstruction under the stated premises.
• Uses B.5.QD and C.11.DUA when continuation matters: choose a useful missing family, new transformation or further calculation.

MATH.8:End

MATH.9 - Determine Whether and How a Choice Rule Can Respect Symmetry

Type: Method Status: Stable Normativity: Normative

MATH.9:1 - Problem frame

Use this pattern when a mathematical rule must choose an answer and transforming the input should transform that answer in the corresponding way. Examples include selecting an element after relabeling a configuration, returning a direction after rotating geometric data, and choosing a solution from problems related by a symmetry.

Start with one transformation that leaves the supplied input unchanged. Ask which permitted answers it leaves unchanged too. This can identify an admissible answer or expose an impossible choice before a selector is implemented.

The method then constructs a rule from one suitable answer for each represented input orbit. It also uses uniqueness, when established, to restrict a solution to the points fixed by the input’s symmetries. A useful result is a compatible choice rule, a restricted candidate to calculate, or a requirement that must change.

The reader needs sets, functions, composition and elementary algebra. MATH.8 supplies group actions, orbits and stabilizers; the definitions needed for the choice argument are restated here. The plane example uses vector length and rotation. If a supplied rule already has the required correspondence, apply it. If the task accepts any answer in the given coordinates and requires no symmetry relation, use an ordinary selection method.

MATH.9:2 - Problem

A problem can allow several answers while supplying no distinction that a requested deterministic rule is allowed to use. An arbitrary tie-break can then violate relabeling or rotation consistency.

Normalization can hide the same difficulty. Two transformations may put the input into the same representative form but return a proposed answer to different places. A common representative alone leaves that choice unresolved.

The task is to determine which permitted outputs respect the symmetries of the supplied input, then extend those choices consistently to related inputs.

MATH.9:3 - Forces

MATH.9:4 - Solution

State the permitted answers and their transformation → find the input stabilizer → choose a permitted fixed answer → extend it along the orbit → construct the needed scope → return the rule or revise the obstructed requirement.

MATH.9:4.1 - State the input, permitted answers and transformation law

Let D be the inputs and Y the possible outputs. Write A(d) for the subset of outputs permitted for input d. An admissible root, minimizing allocation or selected vertex can define this subset.

Give a group G acting on both D and Y. Its action satisfies e*d=d and (g*h)*d=g*(h*d), with analogous rules for outputs; every transformation has an inverse. Different actions on input and output can use the same group elements.

Establish that the permitted answers transform with the input:

A(g*d) = g*A(d),

where g*A(d) means the set of g*y for y in A(d). MATH.8 supplies the solution-preservation argument when it has to be constructed.

The requested deterministic rule f must satisfy both f(d) in A(d) and

f(g*d)=g*f(d).

This relation is equivariance. If the requested output stays unchanged under the transformations, use the trivial output action g*y=y; the relation then expresses invariance.

Keep attributes that the rule is allowed to use inside d. A distinguished label, orientation or mark can change the stabilizer and the existence of a choice. A coordinate label that merely changes under relabeling cannot silently serve as a fixed priority.

MATH.9:4.2 - Find the permitted answers fixed by the input’s stabilizer

The stabilizer of d is the subgroup

K_d = {g in G | g*d=d}.

For every g in K_d, equivariance requires f(d)=g*f(d). Thus the permitted answers for an equivariant rule at d are

B(d) = {y in A(d) | g*y=y for every g in K_d}.

To construct B(d), first obtain the transformations fixing the supplied data, then solve their fixed-point conditions together with membership in A(d). For a finite supplied group and a finite decidable answer set, enumerate those elements and test them. When either is infinite, use an algebraic description or another available construction; a failed finite search leaves the unsearched range open.

If B(d) is empty, no deterministic equivariant rule can answer this input under these requirements. Return the input symmetry and the fixed-output condition that permitted answers fail. This result concerns the supplied data and output requirement; it identifies what a repair must change.

If the original problem has a unique permitted answer y, its preservation under K_d forces every g*y to equal y. The fixed-point equations can therefore restrict or find that answer. Establish existence and uniqueness on the range used by this deduction. With several permitted answers, use the same fixed-point calculation to find a compatible choice; it need not recover every permitted answer.

MATH.9:4.3 - Extend a selected answer over one input orbit

Choose representative data d0 and an answer y0 in B(d0). For input d in the orbit of d0, obtain g with d=g*d0 and define

f(d)=g*y0.

The answer is permitted because the relation in :4.1 carries A(d0) to A(d). It is independent of the transformation used. Indeed, if g1*d0=g2*d0, then k=g2^-1*g1 fixes d0. Since k fixes y0,

g1*y0=g2*(k*y0)=g2*y0.

The rule is also equivariant: for another transformation q,

f(q*(g*d0))=(q*g)*y0=q*f(g*d0).

This constructs the entire rule on that orbit. To evaluate it, retain a way to find g, or an equivalent formula for f(d). An existence argument for g alone may leave the computation unresolved.

If a normalization procedure instead supplies h with h*d=d0, return h^-1*y0. Keeping the direction of this transformation prevents returning a coordinate answer in the normalized frame. The position-selection case in :5.4 carries out both inverse returns.

MATH.9:4.4 - Cover the requested input range

For a finite group acting on a finite input set, enumerate input orbits as in MATH.8. Pick one representative d0 per orbit, compute B(d0), choose one of its members and extend it by :4.3. This supplies a rule on every processed orbit. Empty B(d0) blocks a total rule on a range containing that orbit.

For a larger or infinite range, give the representative construction and a compatible answer for each orbit needed by the claimed rule. These choices can be supplied by formulas or previously established mathematical results. Pointwise nonempty B(d) alone has not provided an evaluation algorithm or the choices across an arbitrary infinite family.

When an existing direct formula can be checked against A(d) and equivariance, use it without building an orbit table. The stabilizer argument can still expose a failed input or explain why its tie-break works.

Before returning the rule, check the other properties actually requested for it. If a geometric or learned model must vary continuously with its data, continuity requires its own argument: the pointwise construction here permits unrelated choices on different input orbits. If the result will be computed repeatedly, compare its evaluation cost with the available direct rule.

MATH.9:4.5 - Repair an obstructed choice

Choose the change that answers the receiving problem.

A supplied distinguished attribute can reduce the stabilizer. Include that attribute and its transformation in the new input, then repeat the fixed-output test. The marked-cycle case below constructs such a rule.

A different output may retain the alternatives the input leaves open. Returning the whole set A(d) respects its induced transformation from :4.1. When A(d) is finite and nonempty, a uniform probability distribution on it does too, if a distribution is the requested result. Sampling a single value is a further calculation with its own randomness and comparison requirement.

An average is usable only when it belongs to the permitted output set and has the required transformation law. The mean of two opposite unit directions is zero, which fails a unit-direction requirement.

The receiving task may instead allow coordinate-dependent choice or a narrower input range. State that changed requirement and construct the corresponding rule. Adding distinctions or weakening a requirement is useful only when the resulting answer serves that task; C.11.DUA helps decide whether obtaining further input is worth its cost when that question is unresolved.

MATH.9:4.6 - Return the result and reopen its changed premise

Return the rule with its input range, permitted output and transformation law, or the obstruction that changes the choice problem. A known unique solution can return a smaller fixed-point calculation instead.

When a criterion, attribute or output changes, recalculate the affected stabilizer and fixed-output condition. Retain orbit calculations and proofs whose premises are unchanged. Small perturbations can remove a tie and reverse a selected answer, so use the changed criterion when the choice depends on it.

Use FPF C.29 to establish what this mathematical result means for another subject. The obstruction for an abstract arrangement leaves available attributes and interventions in a real arrangement to that subject comparison.

MATH.9:5 - Archetypal Grounding

MATH.9:5.1 - Select a cheapest position on a cycle

Four positions are arranged in a cycle with a given clockwise direction. A rule receives real costs c=(c0,c1,c2,c3) and must select one minimum-cost position. Relabeling by k moves position j to j+k modulo 4 and moves its cost with it. The selected position must move in the same way.

Take c=(1,3,1,3). Its minimizers are {0,2}. A half-turn leaves c unchanged but exchanges both permitted answers. Neither is fixed, so B(c) is empty. A deterministic rotation-equivariant selector cannot answer this input. Choosing the smallest coordinate label returns 0 both before and after the half-turn, whereas equivariance requires the result to move to 2.

Now supply a marked position m as part of the input. Choose, among minimizers, the one with least clockwise distance

dist_m(j)=(j-m) modulo 4,

using the values 0,1,2,3. The distances are distinct, so this gives one answer. Under joint rotation of costs, mark and position, dist_(m+k)(j+k)=dist_m(j). The rule therefore respects rotation for every cost vector and mark.

With c=(1,3,1,3) and m=3, the distances of minimizers 0 and 2 are 1 and 3, so the rule selects 0. Rotating once gives costs (3,1,3,1), mark 0 and selected position 1. The same reasoning applies to every rotation.

For the unmarked input, returning {0,2} is a compatible set answer. If a probability distribution is wanted, assign probability 1/2 to each of those positions. Both alternatives retain the choice left open by the input.

A change of costs can also settle it: (1,3,0.9,3) has the unique minimizer 2; (1,3,1.1,3) has the unique minimizer 0. Their closeness to the tied input does not preserve that input’s fixed-point obstruction. It also exposes a discontinuity for a rule required to return one minimizing index as these costs vary through the tie.

MATH.9:5.2 - Restrict a unique optimum by exchange symmetry

Let x1,x2 be nonnegative real numbers with x1+x2=10, and minimize J=x1²+x2². Exchanging the two allocations preserves feasibility and cost.

If the minimizer is known to exist uniquely, the exchange must fix it. Hence x1=x2, and the constraint gives the candidate (5,5). For this example, existence, uniqueness and its optimality can also be established directly: every feasible point has the form (5+h,5-h), and

J(5+h,5-h)=50+2h².

The minimum is attained only at h=0. The direct calculation can finish this small problem; the symmetry deduction is reusable when uniqueness has another available justification.

If the same J is maximized on the segment, its maxima are (10,0) and (0,10). The exchange moves one to the other. Its fixed midpoint is the minimum, so the fixed-point equation alone would solve the wrong optimization question.

Now minimize x1²+2x2² with the same resource constraint. Exchange changes the criterion. Substituting x2=10-x1 gives

J=3*(x1-20/3)²+200/3,

so the unique optimum is (20/3,10/3). The old equality x1=x2 no longer follows. MATH.10 supplies the more general admissible-variation construction when the remaining optimization is the difficulty.

MATH.9:5.3 - Return a direction after geometric normalization

The input is an unordered pair P={-v,v} of opposite nonzero vectors in the plane. The requested answer is one of the two unit directions along its axis. Rotating the input should rotate the selected direction.

For P0={(-1,0),(1,0)}, a half-turn leaves the pair unchanged and negates every permitted unit direction. No permitted output is fixed, so a rotation-equivariant deterministic direction cannot be selected from this input.

The same failure appears in normalization. Both the identity and a half-turn map P0 to the same standard pair. Selecting (1,0) there and undoing those transformations returns opposite directions. The standard pair did not determine a direction of return.

Returning both directions, {-v/|v|,v/|v|}, is compatible with rotation when that set is the required output. Averaging them returns zero, whose length is zero rather than one.

Alternatively, mark one endpoint w in P and return w/|w|. Every rotation R preserves length, so R*w/|R*w|=R*(w/|w|). The marked-input rule is therefore equivariant. It answers a question with additional supplied information, which the unmarked pair lacked.

MATH.9:5.4 - Choose a position despite an ambiguous normalization

Let the six permutations of positions 1, 2 and 3 act on the triples formed by permuting d0=(a,a,b), where a and b differ. An answer may be any of the three positions, and relabeling the triple must relabel the answer.

The transformations fixing d0 are the identity and the swap of positions 1 and 2. All three positions are permitted answers, but only position 3 is fixed by both transformations. Thus B(d0)={3}; choose y0=3.

For the input d=(a,b,a), two transformations normalize it to d0. The first, h1, swaps positions 2 and 3. The second, h2, sends positions 1 to 2, 2 to 3 and 3 to 1. Both carry the b entry to position 3 while placing the two a entries in the remaining positions.

Returning y0 uses their inverses:

h1^-1(3)=2=h2^-1(3).

For every permutation of d0, the transported answer is the position carrying b. This gives the rule on the entire three-input orbit. The stabilizer calculation makes the return independent of the normalizer even though the input initially permits three different answers.

MATH.9:6 - Bias-Annotation

Finite cycles make an obstruction or a constructive repair cheap to display. Larger symmetry groups can make stabilizers, representatives or their transformations expensive to obtain. The rule’s mathematical existence and a feasible evaluation procedure remain different contributions.

A symmetry claim also depends on what is actually supplied. Position names used only for coordinates differ from a distinguished mark the problem permits the rule to use. Keep that difference when translating a real selection problem into the mathematical input.

MATH.9:7 - Conformance Checklist

• The permitted-answer set and both group actions belong to the declared input range.
• The solution relation carries A(d) to A(g*d).
• A selected representative answer is permitted and fixed by the representative’s whole stabilizer.
• Different transformations reaching the same input return the same answer.
• The claimed range has the required representative and answer construction.
• Any changed input, output type or choice requirement is reflected in the returned rule.

MATH.9:8 - Common Anti-Patterns and How to Avoid Them

Use coordinate order as an unannounced priority. The cycle’s smallest-label tie-break fails a half-turn. Supply a distinguished priority that the task permits, or return the alternatives.

Infer a symmetric optimum from a symmetric feasible set. Preserve the criterion and establish the premise needed for the fixed-point deduction. The sum-of-squares maximum and weighted minimum give different answers.

Normalize the input and discard the transformation. An answer in source coordinates needs the inverse return. If several normalizing transformations remain, check their agreement on the proposed output.

Average valid answers into an invalid answer. The zero mean of opposite unit directions is outside the required output set. Test the averaged result’s membership or retain the set.

Call a compatible pointwise rule continuous. The cycle’s minimizing index jumps near a tie. Apply the receiving regularity requirement when it is part of the task.

MATH.9:9 - Consequences

A fixed-output calculation can prevent work on an impossible selector and identify what information or output change would make it possible. Where a compatible answer exists, the orbit construction turns it into a reusable rule for related inputs.

Different representatives can support different valid rules. Their evaluation cost, continuity and usefulness for a receiving task can differ even when each satisfies equivariance. The mathematical construction supplies a comparison basis; the receiving requirements select the rule.

MATH.9:10 - Architectural Rationale

The stabilizer condition is necessary because transformations invisible at the input must leave a deterministic answer unchanged. It is sufficient for extension over one orbit because those same transformations account for every ambiguity in how that orbit is reached. The construction supplies both the impossibility result and its positive counterpart.

MATH.8 generates solution families from an action. This method selects a compatible member and extends that selection across related inputs. A unique solution supplies the fixed-member condition automatically, but several permitted solutions can still contain a suitable fixed member.

A canonical input and a normalizing transformation are different outputs. Choosing the same input representative throughout an orbit is an invariant operation. Recovering an oriented answer additionally uses a transformation and its output action; :5.3 shows why that transformation may not be unique.

Orbit-by-orbit construction is preferable when its fixed-point test settles existence or produces a useful rule. A direct formula can avoid representative search. Set or distribution outputs answer different questions, and geometric continuity can require a construction beyond the pointwise rule.

MATH.9:11 - SoTA-Echoing

Question: when does a symmetry-compatible deterministic choice exist, how can it be constructed, and which changed requirement resolves an obstruction?

Milne, Group Theory v4.01, November 2025, chapter 4 and exercise 4-1 with its solution, characterizes maps between transitive group actions through stabilizers. Adopt that mathematical relationship. The argument in :4.2-:4.4 develops it as a construction constrained by the permitted-answer set. Mathlib’s fixed-point action results, including MulActionHom.map_mem_fixedPoints, supply the corresponding necessary preservation property.

Ma and colleagues, A Canonicalization Perspective on Invariant and Equivariant Learning, 2024, §2.1, distinguishes canonicalized inputs from a single equivariant group-valued canonicalizer, which can be obstructed at inputs with nontrivial stabilizers. Adapt this distinction in :4.3/:5.3/:10. It gives a concrete alternative to assuming normalization has selected a unique return transformation.

Dym, Lawrence and Siegel, Equivariant Frames and the Impossibility of Continuous Canonicalization, 2024, §2.2, separates orbit and group canonicalization and examines continuity; §6 retains stabilizer-related conditions when extending weighted constructions to equivariant outputs. Adopt the separate regularity question in :4.4. Their weighted-frame methods address additional geometric-learning requirements; they are not replaced by the finite construction here.

An arbitrary tie-break is cheaper but can fail the requested transformation law. A supplied direct rule with that law is preferable when it already works. The orbit construction earns its cost by revealing impossible outputs or generating a consistent rule. The cases demonstrate those differences; they do not compare runtimes of geometric-learning implementations.

Reopen when the input attributes, action, permitted answer, demanded regularity or available construction changes.

MATH.9:12 - Relations

• Uses MATH.8: obtain the action, solution-preservation relation, input orbits and stabilizers.
• Uses MATH.2: check independence when a calculation is defined on identified inputs; the stabilizer argument supplies the concrete independence proof here.
• Connects with MATH.7: carry a computed answer through the appropriate inverse map, including its output interpretation.
• Connects with MATH.13: use the existing unique-solution and output-obstruction deductions; this method also constructs the compatible rule.
• Uses MATH.10 when optimization remains: construct admissible variations after symmetry has restricted a candidate.
• Uses C.29 for another subject: recover which supplied attributes and outputs the mathematical choice represents.
• Uses C.11.DUA when further information has a material cost: decide whether acquiring the distinction can improve the receiving choice.

MATH.9:End

MATH.10 - Improve a Mathematical Candidate or Derive a Necessary Condition by Admissible Variation

Type: Method Status: Stable Normativity: Normative

MATH.10:1 - Problem frame

Use this pattern when you have a candidate allocation, shape, history or other mathematical construction under constraints, and need to find an improving change or a condition that an optimum or stationary construction must satisfy.

For example, two allocations obey the same resource limit, but it is unclear how moving some resource between them changes the criterion. Or a proposed physical history has fixed endpoints, and you need to find what its action principle requires of the motion between them. In both cases, construct changes that preserve the relevant constraints, calculate their effect and determine the strength of the resulting conclusion.

The subject of the Method is a family of admissible mathematical candidates and the change of a stated scalar quantity over that family. A variation is a specified change within the family; admissible means that the changed candidate satisfies the conditions retained for this question.

The first useful result is an improving candidate, a necessary condition, a justified minimum or maximum, or a located obstacle to obtaining one. A necessary condition can narrow a search even when it does not settle the optimum.

The reader needs the candidate, its constraints, the quantity being compared and the mathematical operations used to calculate its change. Elementary algebra is enough for the allocation example. The history example additionally uses differentiation and integration. A specialist can supply a construction or theorem at the step where that preparation is needed.

If an available evaluation of a few fixed alternatives already answers the question, use that comparison. This Method is useful when constructing the allowed changes or reasoning from them is the difficulty.

MATH.10:2 - Problem

Changing one value independently can leave the allowed set. A derivative calculated in that direction can then recommend an impossible change. Even with admissible directions, a zero first derivative can describe a maximum, a saddle point or a flat comparison; further reasoning is needed for a minimum.

The reverse difficulty occurs at a constraint boundary: an optimum can have a nonzero derivative because the improving direction is unavailable. A calculation that discards the allowed parameter range loses that conclusion.

These errors share a missing connection between what can vary, what the variation does to the quantity and what the examined family establishes about the original question.

MATH.10:3 - Forces

MATH.10:4 - Solution

Construct an admissible family → calculate the change → derive the condition → establish what it settles → use or revise the result.

MATH.10:4.1 - Fix the comparison

State the candidate, the conditions to retain, the scalar quantity and the conclusion sought. Write the candidate as x and the quantity as J(x) when that notation helps. For minimization, smaller values of J are preferred; for maximization, reverse the comparisons below.

Keep the meaning of J visible. It might be a supplied allocation cost, an approximation error or a physical action functional, which assigns a number to a history. A physical principle can require stationarity of an action without selecting its minimum. Recover that principle and its conditions before using the variational calculation to describe physical behavior.

Distinguish a search for one improving change from a claim of local or global optimality. Local optimality concerns a specified neighborhood of the candidate; global optimality concerns all candidates admitted by the problem.

MATH.10:4.2 - Construct changes that remain admissible

Build a family x(h) with x(0)=x. State the allowed values of the parameter h and substitute the family into the constraints. The parameter may be a scalar, a vector or a discrete choice.

For a fixed total x1+x2=b, the change (x1+h, x2-h) preserves the total. If both components must stay nonnegative, its range is -x1 <= h <= x2. A further capacity limit can shorten that range.

For a history with fixed endpoint values, try q_h(t)=q(t)+h*eta(t), where eta vanishes at both endpoints and has the regularity required by the functional. Check any additional path constraint as well.

A direction tangent to a constraint may preserve it only to first order. At (1,0) on the unit circle, (1,h) has squared length 1+h^2 and leaves the circle whenever h is nonzero. The curve (cos(h),sin(h)) stays on it. Use an admissible curve for a finite comparison, or keep a tangent calculation at the first-order scope its mathematical argument supports.

When a useful family cannot yet be constructed, the missing result is concrete: a parameterized change that retains the named constraint. Obtain the corresponding mathematical construction rather than continue with an inadmissible substitute.

MATH.10:4.3 - Calculate the effect of the variation

Form the difference

DeltaJ(h) = J(x(h)) - J(x(0)).

Substitute the whole changed candidate, including dependent values. Simplify enough to determine the sign or magnitude relevant to the question.

For a differentiable comparison with a scalar parameter h near zero, write

DeltaJ(h) = a*h + r(h), with r(h)/h -> 0,

when that expansion is justified. The coefficient a is the first variation along this family. Higher-order terms or a bound on the remainder can be needed when a vanishes, or when choosing a finite step.

A derivative tells how sufficiently small changes behave under its limit assumptions. To select a particular step, check the finite difference or a bound that covers that step. For a discrete family, compare its admissible members directly; differentiability is not an entry requirement.

If the calculation uses a numerical approximation, relate its error to the sign or comparison being used. C.29.2 develops that computational task. A difference interval entirely below zero can establish improvement for minimization; an interval spanning zero leaves that comparison unresolved.

MATH.10:4.4 - Derive a condition with the allowed directions

For minimization, an admissible h with DeltaJ(h)<0 supplies an improvement. For a local conclusion, use families whose candidates approach the base candidate as h approaches zero, under the neighborhood notion of the problem.

At a local minimum, a differentiable family allowing sufficiently small changes of both signs must have a=0: a positive or negative a would give a decrease in one of those directions. If only small nonnegative h are allowed, the necessary condition is a>=0. For other parameter domains, test the directions actually available.

When a is zero, inspect the remaining change. The differences h^2, -h^2 and h^3 all have zero derivative at zero but respectively give a minimum, a maximum and neither on a two-sided neighborhood. This distinction changes whether the candidate is selected, rejected or needs a stronger argument.

For a vector of variation parameters, keep their joint constraints. Checking one coordinate at a time can miss an improving combination.

MATH.10:4.5 - Establish the reach of the conclusion

Say which candidates the family reaches and which conclusion the calculation proves.

If every admissible candidate can be represented by a member of the family, and DeltaJ(h)>=0 throughout its allowed domain, the base candidate is a global minimizer. If equality occurs only for the base candidate, it is the unique minimizer. An argument restricted to a neighborhood establishes the corresponding local result.

A narrower family can still supply an improving candidate or a necessary condition. Extending that condition to a stronger conclusion requires coverage of the relevant variations or an applicable sufficiency theorem. A convexity argument can sometimes supply the latter; recover its hypotheses before using it. Repeated failure of a chosen local move supplies no general global-optimality guarantee.

For a physical action, derive the stationarity condition required by the physical model. Establish a minimum only if the functional and allowed histories support that stronger conclusion. The free-history example below does so by a nonnegative finite difference.

MATH.10:4.6 - Return the result to the working question

Use the obtained change or condition in the calculation, model or decision that needed it. Keep the admissible family and the reason for the conclusion in the explanation so another practitioner can alter the comparison.

When a criterion changes, recalculate its difference. When a constraint changes, rebuild the parameter domain or family first. B.5.RR helps revise the dependent reasoning while retaining what remains valid.

The mathematical comparison can be completed before any physical change is performed. B.5.MPC supplies the return to physical interpretation and use. If the question is whether an actual intervention causes a result, C.28 supplies the causal-use question.

Stop at the result sufficient for the current use. An improving feasible candidate can be enough to continue; a demand for the global optimum calls for the stronger argument.

MATH.10:5 - Archetypal Grounding

MATH.10:5.1 - Reallocate a fixed total, then change the criterion

Allocate ten divisible units between two uses: x1>=0, x2>=0 and x1+x2=10. The supplied cost is J=x1^2+x2^2. Take the admissible family (x1+h,x2-h), with -x1<=h<=x2.

Substitution gives

DeltaJ(h)=2*(x1-x2)*h+2*h^2.

For an interior candidate, both signs of small h are allowed. The first-order condition gives x1=x2, hence (5,5). At this candidate, the entire finite difference is 2*h^2. Every feasible allocation is (5+h,5-h) for -5<=h<=5, so this proves the unique global minimum, with cost 50.

Now change the cost to J=x1^2+2*x2^2, retaining the total and nonnegativity. The same family gives

DeltaJ(h)=2*(x1-2*x2)*h+3*h^2.

The condition becomes x1=2*x2, giving (20/3,10/3). Its difference is 3*h^2 across the whole feasible interval, so its cost 200/3 is the unique minimum. Keeping the earlier equal split would miss the change introduced by the new criterion.

If the units must instead be whole, x1 and x2 are integers. Completing the square gives J=3*(x1-20/3)^2+200/3; the admissible integer closest to 20/3 is 7. Thus (7,3) has the lowest cost, 67, in that discrete problem. The continuous stationary point helped locate the candidates; the integer comparison settles their use.

Keep the weighted cost J=x1^2+2*x2^2, make the units divisible again, and add x1<=6 while retaining the total and nonnegativity. The previous continuous minimizer (20/3,10/3) is now unavailable. At (6,4), the allowed family has -6<=h<=0 and

DeltaJ(h)=-4*h+3*h^2>=0.

This family covers every newly feasible allocation. Thus (6,4), with cost 68, is the unique global minimizer despite its nonzero derivative along the unrestricted line. The parameter domain carries the decisive information.

These are calculations for the stated cost model. Its use in an allocation decision requires the supplied cost to represent the consequence being compared.

MATH.10:5.2 - Compare histories between fixed endpoints

Consider a one-dimensional free particle with mass m>0, elapsed time T>0, and fixed positions q(0)=0, q(T)=L. The model’s action is

J[q] = integral from 0 to T of (m/2)*(qdot(t))^2 dt.

Take the straight history q0(t)=L*t/T. For any continuously differentiable eta with eta(0)=eta(T)=0, construct q_h(t)=q0(t)+h*eta(t). Expanding the square gives

DeltaJ(h) = (m*h*L/T)*integral eta_dot(t) dt + (m*h^2/2)*integral eta_dot(t)^2 dt.

The first integral is eta(T)-eta(0)=0. The remaining term is nonnegative, and it vanishes for a changed history only when its derivative change is identically zero; the fixed endpoints then force the change itself to vanish. Every continuously differentiable history with these endpoints can be expressed as q0 plus such a change. The straight history therefore uniquely minimizes this functional over that class.

The construction exposes the reason: the fixed endpoints remove the cross term, while every remaining velocity deviation adds a nonnegative contribution.

Now include a restoring potential. In dimensionless variables, use the harmonic-oscillator action J[q]=integral from 0 to 2*pi of (qdot^2-q^2)/2 dt, with q(0)=q(2*pi)=0. At the history q=0, every admissible family q_h=h*eta has zero first variation. Yet the admissible directions eta=sin(t/2) and eta=sin(3*t/2) give respectively DeltaJ=-3*pi*h^2/8 and DeltaJ=5*pi*h^2/8: integration uses integral eta^2 dt=pi and integral eta_dot^2 dt=n^2*pi/4 for these directions with n=1 and n=3. Arbitrarily small changes of both lower and higher action are available. The stationary history is therefore a saddle, not a minimum.

Changing an endpoint condition also requires rebuilding the allowed histories before reusing the free-particle argument. Its vanishing cross term depended on both endpoint values.

This example uses a supplied classical model. Constructing an appropriate action for an unfamiliar physical system is a further physical and mathematical modeling task.

MATH.10:6 - Bias-Annotation

A convenient coordinate can make some changes easy to express and hide others. State what the chosen family reaches before treating its result as a property of all candidates.

A modeler can also import minimization from an allocation problem into a physical action principle. Recover whether the subject requires improvement, an extremum or stationarity; the same variation calculation supports different conclusions under those premises.

For a search procedure, separate a failure to find a better local move from a proof about the full feasible set. This matters when discrete choices or disconnected regions prevent the chosen family from reaching other candidates.

MATH.10:7 - Conformance Checklist

MATH.10:8 - Common Anti-Patterns and How to Avoid Them

MATH.10:9 - Consequences

A constrained comparison becomes a reusable calculation. It can expose a feasible improvement, reduce an optimization problem to a condition or explain why a proposed change cannot help.

The main effort is constructing a useful admissible family and establishing the sign over the range needed by the conclusion. The Method permits an early useful result; full optimization is a larger task when the working question demands it. Keeping the family and argument makes later changes of criterion or constraints easier to handle.

MATH.10:10 - Architectural Rationale

The admissible family, change calculation and conclusion are separated because each can fail independently. A correct difference can describe impossible candidates. An admissible comparison can yield only a necessary condition. A strong mathematical result can still use a criterion that does not answer the practitioner’s question.

Finite differences provide the direct comparison whenever they are manageable. Derivatives expose local structure economically, and sufficiency theorems can extend that information under additional hypotheses. Keeping these routes connected lets the reader use the least machinery that obtains the needed result.

The same construction spans a resource allocation and a continuous history. What carries across is the preservation of conditions and reasoning from the resulting change. The cost model and the physical action retain their different origins and uses.

MATH.10:11 - SoTA-Echoing

For a constrained comparison, the selected approach is to construct feasible changes before interpreting their effect. Direct substitution is useful for small expressions; differential conditions and numerical optimization become useful as the candidate class or calculation grows. The choice depends on the result needed and the assumptions available.

Boyd and Vandenberghe, Convex Optimization, §4.2.3 gives the differentiable convex case: the gradient’s inner product with every feasible displacement characterizes optimality. Adopt its attention to the feasible set and the hypotheses that make a first-order condition sufficient. The Method above also admits nonconvex and discrete comparisons, where that sufficiency cannot be inherited. Specialized convex formulations and algorithms remain useful external constructions when their inputs fit.

Tong, Classical Dynamics, §2.1 develops variations of a history with fixed endpoints and the resulting Euler-Lagrange equations. Adopt the explicit endpoint conditions and the distinction between stationary action and a minimum. This is an established classical source; it supplies neither an action for every new physical system nor its empirical justification.

C.29 supplies the mathematical interpretation and return, while C.29.2 supplies computational formulation and error-sensitive use. Here the reusable contribution is construction of the admissible family and the argument from its change. If those operations require a specialized variational, optimization or physical-modeling technique, recover that technique at the point where the needed result becomes specific.

Revisit the construction when constraints, regularity, candidate class or the required conclusion change. A newer solver can improve cost without changing the meaning of the admissibility and optimality claims.

MATH.10:12 - Relations

• C.29 connects the mathematical candidates and conclusion to the original subject and working question.
• C.29.1 establishes the transfer of a result when a change of representation could lose a relevant distinction.
• C.29.2 constructs a computation and relates numerical error to the comparison being used.
• B.5.RC and B.5.RA help recover a needed mathematical construction or argument; B.5.RR revises dependent reasoning after a premise changes.
• B.5.MPC connects the physical account, mathematical construction, computation and use. C.28 handles a causal consequence attributed to an intervention.

MATH.10:End

MATH.21 - Construct an Object through Convergent Approximations

Type: Method pattern Status: Stable Normativity: Normative unless marked informative

MATH.21:1 - Problem frame

Use this pattern when a number, function, infinite structure or other mathematical object is to be obtained from increasingly informative constructions, and the work needs to establish what their limit is and what can be done with it. A formula, finite prefix or finite family can describe an approximation even when the object it describes is infinite.

The governing question is what the receiving argument or operation must retain as approximation improves. Examples include a value within a tolerance, the settled first part of an infinite sequence, or a function whose integral or derivative can be obtained from approximating functions. These requests can require different notions of convergence.

First useful move: state one requested observation or operation on the intended object, then find a condition under which an approximation supplies it. A shrinking interval can answer a numerical tolerance request. A compatible prefix can answer a request for finitely many entries. This gives a usable result before constructing every property of the limiting object.

The reader needs elementary reasoning about functions, sequences and inequalities. The numerical case introduces its use of real completeness; the function case also uses elementary differentiation. Other spaces require the knowledge needed to state their convergence and operations.

Use an already supplied object or applicable limit theorem when it answers the question. Use the fuller method when existence, retained structure, or use of a finite approximation remains unresolved. Physical adequacy and computational realization add their own questions to the mathematical construction.

MATH.21:2 - Problem

Finite stages can look increasingly satisfactory while leaving the mathematical result undetermined. The intended limit may be absent from the chosen space. Agreement at each fixed input may fail to control all inputs together. An operation valid on every stage may cease to be valid at the limit.

Even established convergence can leave a practical question open: which stage supplies the requested result? Conversely, a finite observation can be available before an entire limiting construction has been resolved. The method must connect the convergence claim to the particular subsequent use.

MATH.21:3 - Forces

MATH.21:4 - Solution

Local mantra: name the limiting object and its next use; construct the approximation family; choose and establish convergence; obtain the object in the admitted space; carry only the justified properties and operations; return a sufficient finite result or the remaining mathematical question.

MATH.21:4.1 - State what approximation must preserve

Name the space of intended objects, the approximating objects and how the latter are compared with the former. If they initially have different kinds, supply an embedding or interpretation. For example, a rational number can approximate a real number; a finite word can determine the beginning of an infinite word.

State the requested result. Does the receiver need a value, an operation on the limit, an existence theorem, or a finite observation? For a numerical use, specify the error quantity and tolerance. For a prefix use, specify which entries must be settled. The mathematical question determines the approximation requirement.

Choose a convergence notion that supports that result. In a metric space, with distance d, a sequence x_n converges to x when, for every positive epsilon, all sufficiently late terms satisfy d(x_n,x)<epsilon. For functions, pointwise convergence allows the sufficiently late index to depend on the input; uniform convergence requires one index to work for all inputs in the named set. For infinite words, convergence can mean eventual agreement on every fixed finite prefix.

These are different constructions of the convergence requirement. Use their definitions to decide what they permit. Numerical distance is useful when it measures the requested difference; finite observation or another mathematical relation can be more suitable elsewhere.

MATH.21:4.2 - Construct and compare the finite stages

Give the approximating rule and establish the relations on which improvement depends. For nested intervals, prove containment and decreasing width. For compatible prefixes, prove that later stages retain the earlier entries. For a series or iterative construction, obtain a bound on the unresolved remainder.

The same argument must cover the stages used by the conclusion. A finite sample can suggest a bound or expose a failure; a claimed statement about all later stages needs the corresponding argument.

When the candidate limit is not yet available, a Cauchy condition can express progress using only the approximations. In a metric space it says: for every positive epsilon there is N such that d(x_m,x_n)<epsilon whenever m and n are at least N. This compares the entire remaining tail.

If a stopping rule uses only successive changes, derive how they bound the remaining tail. Successive changes of size 1/n become small, yet their accumulated sum is unbounded. A summable bound, a contraction estimate or another proved remainder relation can make a successive-change test useful.

Retain a cheaper construction when it already supplies the requested observation. Refinement need not improve every property at every stage.

MATH.21:4.3 - Obtain the limit where it is needed

If a candidate object is already available, prove convergence to it by the selected definition or a suitable theorem. Otherwise use an existence result whose conditions the approximation satisfies.

For example, completeness of a metric space means that every Cauchy sequence in it has a limit there. Establishing a Cauchy condition and applying a known completeness result can obtain an object without guessing its closed form. A local existence argument may suffice even when the whole space is incomplete.

When the limit falls outside the original objects, decide whether the receiving work admits an extension. Construct the new objects and the embedding of the old ones; prove the properties the subsequent work will use. One route takes suitable Cauchy sequences as representations and identifies those whose mutual distance tends to zero. MATH.2 supplies the quotient operation: operations on equivalent representatives must produce equivalent outputs, so the quotient result is independent of the representative. The real-number construction is one instance of this route.

Establish uniqueness when the receiver needs a single result. In a metric space, if x_n tends to both x and y, the triangle inequality gives d(x,y)≤d(x,x_n)+d(x_n,y); the right side can be made arbitrarily small, so x=y. Other convergence structures need their own uniqueness condition or an explicitly retained class of possible limits.

If convergence or existence fails, return the failed condition and the still valid finite information. That can suggest a different space, a different approximation family, or a weaker requested conclusion.

MATH.21:4.4 - Pass properties and operations through the limit

For every operation used next, establish the relevant interchange. If F is continuous for the chosen source and target convergence, x_n→x gives F(x_n)→F(x). The argument can be local to this family; global continuity is sufficient in many cases but is more than every use needs.

Check the property actually consumed. A limit of objects in a closed subset remains in that subset. Other properties can disappear: finite words padded with zeros can converge to an infinite word with infinitely many ones.

For a function limit, distinguish a claim about its values from a claim about integration or differentiation. The required limit theorem may ask for uniform control, domination, or another hypothesis specific to the operation. In :5.3 a uniform value bound supports integration over a finite interval, but it does not support differentiating the approximations to obtain the limiting derivative.

When an interchange fails, retain the established limit and repair the affected operation. Strengthen the convergence condition, choose another family, restrict the domain, or calculate that operation by a different argument. Select the repair from the receiver’s need.

MATH.21:4.5 - Obtain a sufficient finite result

Translate the receiving request into a condition on a stage. If an established bound gives d(x_n,x)≤e_n, a stage with e_n within the requested tolerance supplies the approximation. For nested numerical intervals, the midpoint has error at most half their width. For compatible prefixes, a stage containing all requested entries supplies them.

When execution must find that stage, provide either an obtaining rule or a recognizable stopping condition with a reason it will be reached. An explicit rate of convergence is one option. An enclosure whose width can be checked during refinement may suffice without a rate fixed in advance.

A residual is useful only through its established relation to the requested error. A small equation residual can accompany a large error in the unknown; the comparison needed by the use must connect them.

Return the approximation with the mathematical bound or settled observation it supplies. If only existence has been established, retain that result and identify the missing obtaining procedure for a computational continuation. Numerical conditioning, finite arithmetic and execution cost belong to that continuation.

MATH.21:4.6 - Use and revise the construction

Use the limiting object in the argument, or use the finite result for the selected observation. Keep the convergence notion and any condition needed by the next operation with that use.

A changed tolerance can require a later stage. A changed operation can require a stronger convergence result. A changed space can remove existence or uniqueness. Reopen the affected argument and retain the finite constructions and proved consequences that survive.

In modeling, interpret the resulting mathematical consequence against the subject using C.29 and the corresponding modeling method. The approximation’s mathematical convergence and its ability to answer the subject question remain separately assessable.

MATH.21:5 - Archetypal Grounding

MATH.21:5.1 - Obtain a real object from rational intervals

The task is to construct a positive number r with r²=2 and obtain rational approximations with a chosen absolute error.

Start with l_0=1 and u_0=2. At each step take the rational midpoint m. If m²≤2, replace the lower endpoint by m; otherwise replace the upper endpoint. Squaring is increasing on the positive interval, so each step retains l_n²≤2≤u_n². The intervals are nested and their widths are 2⁻ⁿ.

The lower endpoints form a bounded increasing sequence. In the real numbers, their supremum r exists. Each l_n≤r≤u_n: every later lower endpoint is at most u_n, and earlier ones are no larger than l_n. The shrinking width makes this r the only common point.

Both r² and 2 lie between l_n² and u_n². Since the endpoints stay between 1 and 2, the width of this squared interval is (u_n-l_n)(u_n+l_n)≤4·2⁻ⁿ. It tends to zero, so r²=2. This obtains the desired object without presupposing a square-root value to drive the construction.

After four bisections the interval is [22/16,23/16]. Its midpoint 45/32 differs from r by at most 1/32. For a smaller tolerance epsilon, choose a stage with 2⁻ⁿ⁻¹≤epsilon, or refine until the interval width is at most twice epsilon.

Changed space. If the result must remain rational, existence fails. In a fraction p/q in lowest terms, p²=2q² would make p even, and then q even, contradicting lowest terms. The rational approximations and their widths remain available, but they construct a real number rather than a missing rational solution. The next decision concerns admitting that extension or retaining a finite rational answer.

MATH.21:5.2 - Construct an infinite word and return a finite observation

Let p_n be a binary word of length n, with p_n a prefix of p_(n+1). Positions start at zero. Define b(k) to be entry k of p_(k+1). Compatibility makes that entry agree with every later prefix, so b is an infinite binary word whose first n entries are p_n.

For a common space of approximations, pad each p_n with zeros to obtain an infinite word b_n. Use convergence by eventual agreement on each finite prefix. For a request about the first m entries, every b_n with n≥m agrees there with b. This proves convergence and gives the return stage: p_m supplies those entries. Any calculation depending only on them, such as their count of ones, can use that finite result.

The global property “has only finitely many ones” does not pass to this limit. Take p_n to consist of n ones. Each zero-padded b_n has finitely many ones, but b has a one at every position. A question about a fixed finite prefix is settled; a question about the entire tail needs another argument.

The construction uses a consistency relation between finite stages and a rule for obtaining every entry. Its computational realization additionally needs a way to obtain the required p_m. Merely knowing that such prefixes exist does not supply their generator.

MATH.21:5.3 - Preserve values and integrals, then inspect differentiation

For n≥1, let f_n(x)=sin(nx)/n on [-1,1]. The inequality |f_n(x)|≤1/n holds for every input in the interval. Thus the functions converge uniformly to f(x)=0.

For a requested value error epsilon, n≥1/epsilon is sufficient. Integration over the interval is also controlled: the absolute integral of f_n-f is at most 2/n, by the interval length and the uniform bound. This estimate supplies an integral-error result without depending on cancellation of positive and negative values.

Now ask for the derivative at zero. Each f_n has derivative cos(nx), so f_n’(0)=1 for every n. The limit function has f’(0)=0. The value convergence therefore fails to justify passing this operation through the limit, even at that one point.

One possible sufficient repair, for differentiable functions on a common open interval, is pointwise convergence of the functions together with locally uniform convergence of their derivatives. A suitable limit theorem then identifies the limiting derivative. The present f_n fail that condition. If the construction can change, a family with controlled derivatives can support the stronger use; if it must stay fixed, obtain the derivative of its limit by another argument.

The result retains uniform convergence and its finite value and integral bounds. Only the derivative interchange has been refused. This is why the requested next operation belongs in the initial choice of approximation.

MATH.21:6 - Bias-Annotation

Numerical examples can make convergence look like increasing decimal accuracy. The prefix case exposes another form: agreement on finitely many observations of an infinite object. Function examples show that even numerical convergence has different strengths according to the subsequent operation.

The examples use ordinary classical mathematics. An effective or constructive account must retain the obtaining information its logic and representation require. A user of a known complete space can apply its theorems directly; a constructor of a new space must establish the relevant properties of that construction.

MATH.21:7 - Conformance Checklist

For the proposed construction:

• The intended space, approximation family and comparison between their objects are stated.
• The receiving observation or operation determines the convergence requirement.
• The general argument covers the stages claimed, including the unresolved tail when it matters.
• The limit exists in the admitted space, or the required extension is justified.
• Uniqueness and representative independence are established where the subsequent use needs them.
• Each retained property or limit interchange has its applicable condition.
• A finite return supplies the requested error or observation; an executable return has an obtaining or stopping rule.
• A failed condition leaves the remaining valid construction and a useful next question identifiable.

MATH.21:8 - Common Anti-Patterns and How to Avoid Them

Small increments used as a tail bound. The harmonic increments in :4.2 shrink while their sum grows. Derive a remainder estimate before using such an increment to decide that the requested approximation has been reached.

An absent limit treated as an object of the original space. The intervals in :5.1 have no rational point in common. Admit the real extension or return a finite rational approximation.

A property inherited merely because every stage has it. Each padded word in :5.2 has finitely many ones; its limit does not. Establish preservation for the particular property.

A value approximation used for a different operation. The functions in :5.3 approximate values uniformly but supply the wrong limiting derivative at zero. Inspect the interchange needed by the operation.

MATH.21:9 - Consequences

The method can obtain new objects, justify a finite use of them, and localize the reason a proposed use fails. A family can remain valuable even when one requested operation does not pass to its limit.

Changing the space, convergence relation or preserved operation can open a further mathematical problem. Those changes also create different modeling and computational possibilities, whose additional costs and subject conditions can then be compared.

MATH.21:10 - Architectural Rationale

Approximation is a construction through a relation between stages and a result. The relation determines what information accumulates and what a finite stage can supply. This explains the common method across rational intervals, prefixes and functions without making their convergence definitions interchangeable.

Existence, identification of equivalent constructions, preservation of operations and finite return are connected tasks. Quotient construction handles identification; proof construction supplies missing implications; convergence and continuity supply the limiting passage. Keeping their contributions explicit lets a changed operation reopen the relevant mathematical step.

A stronger notion of convergence is useful when it supports a needed consequence. A weaker one is sufficient when it already supplies the receiver’s observation. This permits economical use of mathematical results while preserving their conditions.

MATH.21:11 - SoTA-Echoing

The working question is how a family of approximations supplies an object and the operations needed on it. The selected line combines a convergence relation, an existence argument in the chosen space, preservation of the required operations, and a finite-use condition.

Avigad, Lewis and van Doorn’s Logic and Proof, §§21.3-21.4 develops the Cauchy-sequence quotient and completeness of the reals. Its construction informs :4.3: specify when approximation families represent the same object and make arithmetic respect that identification. An existing completeness theorem is a cheaper alternative when its space already fits; constructing a new completion is useful when a missing object prevents the intended operation.

Mathematics in Lean, chapter 11 organizes convergence and continuity through filters, while exposing metric versions for ordinary calculations. This supports the generality of :4.1/:4.4 without requiring filter notation for every use. Mathlib’s current uniform convergence and limits of derivatives give inspectable statements with different hypotheses. They inform the operation-specific repair in :5.3. Repeated numerical agreement cannot replace those hypotheses; an applicable theorem can avoid repeating its proof.

Bauer and Kavkler’s A Constructive Theory of Continuous Domains Suitable for Implementation, 2008, is an implementation-oriented methodological anchor. It compares prescribed approximation rates with interval representations that test a requested width during computation, keeping the logical assumptions of that implementation explicit. The adopted contribution to :4.5 is the choice between a supplied rate and a justified stopping observation. Its particular logic and real-number implementation are alternatives for that branch, not requirements on every convergent construction.

Use the weakest established condition that supports the requested result. Reopen the comparison when the space or operation changes, when a claimed approximation cannot be obtained, or when a different representation supplies the same use with less work. These sources support the stated constructions; choosing a particular numerical algorithm remains a further task.

MATH.21:12 - Relations

• MATH.2 identifies equivalent representations and carries well-defined operations to their quotient.
• MATH.19 constructs an existence, convergence or preservation argument when an intermediate implication is missing.
• MATH.18 compares different mathematical accounts of a limiting construction.
• MATH.22 changes assumptions when a needed limit or operation is absent; MATH.23 develops the resulting conjecture.
• C.29 interprets the mathematical consequence in its subject. Modeling methods choose the subject-relevant approximation and computational methods obtain its finite realization.
• B.5.QD and C.40.CD develop the next useful question after a construction, obstruction or changed use.

MATH.21:End

MATH.22 - Change Axioms and Trace Their Consequences

Type: Method pattern Status: Stable Normativity: Normative unless marked informative

MATH.22:1 - Problem frame

Use this pattern when a mathematical assumption excludes a construction you need, a theorem uses a stronger premise than its intended application supplies, or two accounts differ in what they assume. The work is to change the assumptions and establish what the changed theory permits.

An axiom is a statement taken as a premise of the theory being developed. A model of those axioms is a mathematical structure in which they hold under a stated interpretation. For example, an ordered set interprets an order relation; a collection of permutations interprets composition. This use of model concerns mathematical satisfaction. Applying the structure to an observed subject requires the additional correspondence work in C.29 and MMP.

First useful move: isolate one assumption and one construction or conclusion affected by it. Try to derive that conclusion from the remaining assumptions, or construct a case where they hold and the conclusion fails. The result identifies what can be retained and what must change.

The reader needs elementary reasoning about sets, operations, relations and their laws. The examples introduce the group, order and arithmetic assumptions they use. A change of logical inference rules needs the corresponding knowledge of that logic.

If a supplied theorem already works under the available assumptions, apply it. MATH.6 suffices for refuting one proposed consequence. Use the present method when the receiving work needs a revised theory, its changed constructions and its surviving results.

MATH.22:2 - Problem

A familiar axiom set can make a useful construction impossible or unnecessarily restrictive. Dropping a premise admits more structures, but a familiar proof may then fail. Adding a convenient operation can conceal an existence assumption, and adding a desired law can conflict with laws already retained.

There are different outcomes to establish. A proof might survive unchanged, admit a new proof, need an extra condition, or have a counterexample. A stopped proof search leaves these possibilities unresolved. The revised theory must expose the difference because later reasoning and computation consume its consequences.

MATH.22:3 - Forces

MATH.22:4 - Solution

Local mantra: isolate the assumption and wanted construction; choose the change; build or interpret the changed structures; trace the affected arguments; establish what the comparison warrants; return the revised theory to use.

MATH.22:4.1 - Identify the assumption and its mathematical job

State the objects, operations and laws currently used. Find the step where the disputed assumption enters. It may justify rearranging operations, comparing two objects, choosing an element, taking a limit, or introducing an object with a required property.

Distinguish a law about the objects from a logical rule used to infer statements about them. Removing commutativity changes the structures being studied. Restricting proof by contradiction can change the permitted arguments even when the question concerns the same objects.

State the desired gain. Examples include admitting noncommuting operations, retaining incomparable alternatives, obtaining a missing limit, or preserving the computational content of a proof. This gain guides which consequences to examine first.

For a local question, the relevant definitions and proof dependencies are enough. Reconstruct a whole formal foundation only when the conclusion being sought depends on it.

MATH.22:4.2 - Choose the change and what stays fixed

With a fixed language and logic, removing axioms weakens the theory: every old model still satisfies the retained axioms, and additional models may become possible. Adding axioms strengthens it: every new model must satisfy the old axioms as well, so some old models may be excluded. Replacing an axiom combines removal and addition; neither direction of inclusion follows automatically.

Name the fixed assumptions and the changed one. If the vocabulary changes too, give the interpretation used to compare the accounts. MATH.18 develops that comparison.

When introducing a symbol for an operation, ask how the operation is obtained. An abbreviation such as d(x,y)=x+(-y) expands into operations already available. If a proposed definition instead asks for the unique object satisfying a property, establish existence and uniqueness on its intended inputs. Calling it a definition does not complete that construction. In :5.2, a least upper bound exists in one order and is absent in another.

An added operation can also require a larger collection of objects. In that case construct the extension and the map from the earlier structure, then establish which old operations and relations the map preserves. MATH.1/.2/.16 supply construction methods for objects and operations. An extension by limits also requires specifying convergence and establishing that the needed limiting objects exist.

MATH.22:4.3 - Construct models and separating cases

Give the objects and the interpretation of every operation and relation needed by the claim. Establish each retained axiom. For an infinite family, use a general argument; enumerated cases suffice only when they exhaust the admitted possibilities.

Choose a case that distinguishes the changed theories. To investigate an axiom A relative to retained assumptions T, a model of T in which A fails shows that A is not a consequence of T. A model where A holds shows that adding A is compatible with that model. These are different results, and both can matter.

Use MATH.6 to construct a countermodel. Finite structures are often a cheap first attempt because their operations and relevant failures can be displayed completely. An existing infinite structure with a short argument may be simpler.

If the changed account uses different objects or primitives, an interpretation can carry its constructions into an established theory. Check the translated axioms and the translated steps of inference needed for the result. A picture suggesting an analogy is a starting point for this work.

MATH.22:4.4 - Trace the consequences that the receiving work uses

For each required result, locate the affected proof step.

• Retain a proof when its steps use only assumptions that remain.
• Try another proof when the old one uses the removed assumption. A dependency of one proof need not be a necessary premise of the theorem.
• Keep a conditional result when the receiving use can supply the additional premise.
• Return a countermodel when the conclusion fails under the revised assumptions.
• Leave a particular consequence unresolved when neither an argument nor a countermodel has been obtained.

Apply the same reasoning to constructions. Check whether their inputs are still admitted, the operations remain defined, and the properties used by the next step still follow. For example, :5.1 retains cancellation after dropping commutativity but loses unrestricted rearrangement of factors.

When a proof is formalized, its recorded dependencies can help find affected steps. They report what that proof uses. A claim that no proof can avoid an axiom requires an additional argument.

If the result will generate data or a program, trace what the new principle supplies operationally. An existence argument and an effective construction support different next uses. MATH.12 handles extraction; the relevant computational method handles execution and cost.

MATH.22:4.5 - State what the model or proof establishes

In a sound interpretation of a deductive system, a proof preserves truth in every model of its premises. Therefore a model of T where A fails rules out a proof of A from T. If another model of T satisfies A, it likewise rules out a proof of not-A. Together these establish that A is independent of T, relative to the logic and semantics being used.

A model also supports consistency: a sound derivation of a contradiction from its axioms would have to make a contradiction true in that model. The construction of the model relies on background mathematics. Keep that dependence when reporting a consistency result, especially when comparing foundations. A failure to find a contradiction supplies no such construction.

For a definitional extension, expand the new symbols in the affected claims and arguments. When all new operations are definable in the old theory and the definitions can be eliminated, conclusions stated wholly in the old language retain their old justification. If an existence principle or inference rule has been added, examine its consequences separately.

The preceding model arguments use their stated semantics. A change to intuitionistic, dependent-type or another logic requires an interpretation sound for its own rules; an arbitrary transfer of classical model arguments could answer the wrong question.

MATH.22:4.6 - Use the revised theory

Return the changed assumptions together with the construction, theorem or obstruction needed by the receiving work. Carry the conditions under which it can be used. An unresolved consistency or consequence question can be handed to a collaborator without presenting it as settled.

Choose between revised theories by the work they enable and the costs they impose. One can admit more objects, another can make a needed construction available, and another can retain an effective procedure. FPF’s ordinary characterization and choice methods apply when these alternatives must be compared; the present method supplies their mathematical consequences.

Use the changed result to reformulate a model, modify a method, or pose the next mathematical problem. For a new conjecture, state which further relation might hold under the retained assumptions. A later failure reopens the assumption or inference on which the failed use depends.

MATH.22:5 - Archetypal Grounding

MATH.22:5.1 - Drop commutativity while preserving invertible composition

Suppose a collection has an associative operation, an identity e and an inverse for every element. These are the group assumptions. Add commutativity, xy=yx, and familiar rearrangements become available. For example, MATH.19’s argument proves (xy)^n=x^n y^n.

The intended new use composes invertible operations whose order matters. Remove commutativity and retain the group assumptions.

Cancellation survives, although its proof may change. A commutative proof multiplies ax=ay on the right by the inverse of a, then rearranges axa⁻¹ and aya⁻¹ to obtain x=y. This uses commutativity. A replacement proof multiplies on the left: a⁻¹(ax)=a⁻¹(ay). Associativity gives (a⁻¹a)x=(a⁻¹a)y, hence x=y by the inverse and identity laws. The theorem therefore survives after removing commutativity.

Unrestricted rearrangement fails. Consider all permutations of {1,2,3}, composed with the rightmost permutation acting first. Composition is associative, the identity leaves each element fixed, and each bijection has an inverse. Let f swap 1 and 2, and let g swap 2 and 3. Then fg sends 1 to 2 to 3 to 1 as a cycle, while f² and g² are identities. Thus (fg)² sends 1 to 3, but f²g² sends 1 to 1.

This is a model of the group assumptions with noncommuting elements. The two-element group {e,h}, with h²=e, is a model where every pair commutes. Under ordinary classical group logic, the two models show that commutativity is independent of the retained group axioms.

The revised theory now admits ordered compositions. It retains cancellation and inverses. Rearrangement remains usable for particular pairs whose commutation is established; it has ceased to be a general permission.

MATH.22:5.2 - Remove total comparability and inspect a proposed new operation

A partial order is reflexive, antisymmetric and transitive. A total order additionally compares every pair: x<=y or y<=x. Suppose the work needs to retain pairs for which neither direction holds.

Remove total comparability. On pairs of natural numbers, define (a,b)<=(c,d) when a<=c and b<=d. The three partial-order laws follow coordinate by coordinate. The pairs (1,0) and (0,1) are incomparable. The ordinary order on natural numbers supplies a model with total comparability; the pair order supplies a model without it.

Now ask for a least common upper bound of two objects. In the pair order, it is the coordinatewise maximum. It is above both inputs, and any common upper bound is above each coordinatewise maximum. This proves both the construction and its leastness.

The partial-order axioms alone do not supply that operation. Take four distinct objects a,b,u,v. Besides reflexive comparisons, require a<=u, a<=v, b<=u and b<=v, and no others. This is a partial order. Both u and v are upper bounds of a and b, but neither is below the other; a and b are not upper bounds. There is no least upper bound of the pair.

Consequently, writing “x join y” for every pair in an arbitrary partial order adds an existence requirement unless a construction has already supplied it. The work can select an order where joins exist, add the join assumption and accept its narrower class of models, or undertake a construction that enlarges the objects. Choosing one of u or v alone supplies an upper bound, not the missing least one.

This separates two changes that a generic instruction to “relax the order” would hide: allowing incomparability and requiring a combining operation. A model of alternatives can use the resulting order; any decision to prefer one alternative remains a separate choice.

MATH.22:5.3 - Introduce total reciprocal notation without retaining a false law

Suppose arithmetic uses field laws, including 0!=1 and distributivity, and the reciprocal law x*inv(x)=1 for x!=0. The proposed change makes inv a total operation and asks that same law to hold at zero.

The retained laws already imply 0*y=0. Indeed, (0+0)*y=0*y+0*y by distributivity, and cancelling one 0*y from 0*y=0*y+0*y leaves 0=0*y. The proposed new reciprocal law at zero would therefore imply 0=1. The retained assumptions and the new law conflict.

A different change works: over the rational numbers, define inv(0)=0 and inv(x)=1/x for x!=0. This gives a total operation, retains the nonzero reciprocal law, and leaves the field operations unchanged. It has not made cancellation of a zero factor valid.

For a use involving the equation x*y=x*z, cancellation still requires x!=0. At x=0, all rational y,z satisfy the equation. A calculation using total reciprocal notation must retain that condition or inspect the zero case.

The result is a consistent construction within rational arithmetic and a revised law with its condition, rather than the initially requested unconditional inverse law. Total notation and stronger algebraic permission have been separated.

MATH.22:6 - Bias-Annotation

Familiar structures can make their extra laws feel unavoidable. The permutation and partial-order cases expose assumptions that integers with addition or a single numerical scale can conceal.

The examples use elementary classical structures so that the changed laws can be inspected directly. They demonstrate the method without deciding between competing foundations of mathematics. A foundational change needs its own interpretation and consequences, including any change in constructive use.

MATH.22:7 - Conformance Checklist

For the change being made:

• The altered axiom, definition or inference rule and the assumptions retained are identifiable.
• The desired construction or consequence explains why the change is useful.
• A claimed model supplies the required objects and interpretations and satisfies every retained axiom.
• A definition has its required existence and uniqueness, or the additional assumption is stated.
• Reused proofs survive at the steps that matter; a lost proof is distinguished from a refuted theorem.
• Independence, consistency and non-derivability claims have the appropriate model or argument and retain their background assumptions.
• The receiving use gets the revised consequence with its applicability and any obtaining procedure still needed.

MATH.22:8 - Common Anti-Patterns and How to Avoid Them

Removing a premise while retaining its rewrite permission. Dropping commutativity in :5.1 permits noncommuting operations. Reordering their factors requires a local commutation argument.

Defining an object that need not exist. The four-object order in :5.2 has common upper bounds but no least one. Supply a construction or change the assumptions before using join as a total operation.

Extending notation and silently strengthening a law. Total reciprocal notation in :5.3 is available with a conditional inverse law. The unconditional law contradicts the retained arithmetic.

Treating a failed proof as independence. The proof may need a different lemma. Establish non-consequence through a separating model or a suitable metatheoretic argument. For the model route in :4.5, establish both directions of separation before claiming independence.

MATH.22:9 - Consequences

The result exposes which generalizations preserve a useful conclusion, which additions buy a new construction, and which changes require a different problem. A small separating structure can prevent repeated attempts to derive a false consequence.

Changing axioms can also open a family of new questions. Which maps preserve the revised structure? Which previous constructions still work? Can a missing operation be supplied by extending the objects? These questions continue the mathematical development and give modeling or methodological work new usable constructions.

MATH.22:10 - Architectural Rationale

A proof states what follows from assumptions. A model makes their simultaneous satisfaction and separating consequences inspectable. Using both permits directed theory change: follow a needed construction to its assumptions, change them, and return the consequences to that construction’s use.

MATH.6 constructs countermodels, MATH.18 compares accounts through interpretations, and MATH.19 constructs missing arguments. Here these methods support a revised theory whose consequences can be used deliberately.

Logical consistency, mathematical fruitfulness and correspondence to an observed subject answer different working questions. The first controls what the axioms jointly permit; the second concerns the further constructions and questions they open; the third requires subject knowledge and observation. Their connection supports mathematical modeling without making one stand in for the others.

MATH.22:11 - SoTA-Echoing

The working question is how to change mathematical assumptions while retaining justified and useful consequences. The selected line combines proof-dependency analysis, construction of models and interpretations, and explicit separation of definitional change from added principles.

Adopt the model-and-consequence method. The Open Logic Project’s Models and Theories makes the relation between axioms and satisfying structures explicit. Logic and Proof, §§10.1-10.5 supplies interpretation and soundness for the first-order branch. These are method sources for :4.3/:4.5. Their use defeats an inference from unsuccessful proof search to non-consequence: a separating structure supplies the needed reason. A known theorem or short existing interpretation is cheaper when it already settles the same question. The chosen branch accepts the cost of constructing a model when that difference remains unresolved.

Adapt dependency analysis to the required return. Theorem Proving in Lean 4, Axioms and Computation explains how added principles affect proof and computational interpretation, and how axiom dependencies can be inspected. This changes :4.1/:4.4: trace the principle actually used and what a later construction can obtain. Reading a proof’s dependencies is a useful alternative to rebuilding it. That inspection alone does not settle whether another proof avoids the principle. A non-derivability claim needs a separate argument, such as a separating model under the stated soundness assumption. The source describes one formal system; Lean use is optional, and its evaluation mechanisms are not generalized to all mathematics.

Retain these approaches while their constructions answer the local question at acceptable effort. Reopen the comparison when the logic changes, a proposed interpretation fails, another proof removes the alleged dependency, or the receiving use needs computational content that the revised theory has not supplied.

MATH.22:12 - Relations

• MATH.6 constructs a countermodel; MATH.18 compares accounts through interpretations.
• MATH.19 constructs or replaces affected arguments; MATH.12 recovers their constructive output.
• MATH.1/.2/.16 supply construction methods when a changed theory needs different objects or operations.
• B.5.FM, B.5.TC and C.29 use the resulting assumptions and structures in reformulation, theory change and correspondence to a subject.
• MMP and the relevant CMP methods use the revised mathematical construction, adding subject interpretation or an executable procedure when required.
• Core’s Method-development family can use this mathematical account to change formal descriptions of methods; the behavior of the described work still needs its own justification.

MATH.22:End

MATH.23 - Develop a Conjecture by Changing a Construction

Type: Method pattern Status: Stable Normativity: Normative unless marked informative

MATH.23:1 - Problem frame

Use this pattern when a mathematical construction works in some cases, fails after a change, or reveals a relation that could support a new theorem. You need to formulate the next claim and a way to investigate it.

A conjecture is a mathematical assertion proposed for investigation. Developing it includes choosing its objects, assumptions, quantifiers and conclusion. The result can become a theorem, a refuted claim, or a more useful question. Its value lies in what the answer would let someone construct, infer, explain or change.

First useful move: change one mathematically consequential part of the construction and compare what happens. Replace a parameter by a variable, combine two outputs, remove a used assumption, or ask the same operation to preserve another property. Try the changed construction and identify the equation, condition or obstruction that controls its result.

The reader needs the mathematical operations used by the starting construction and elementary proof reasoning. The examples explain their additional operations; the last example develops a limit argument. The method can be performed by a person, an AI agent or cooperating contributors with the needed preparation.

Use an established result when it already answers the question. MATH.19 helps prove a sufficiently clear claim. B.5.QD develops questions more generally. Here the work develops a mathematical assertion through construction, variation, proof analysis and counterexamples.

MATH.23:2 - Problem

A list of successful cases leaves many possible general claims. A formula can match every computed value and fail beyond them. A proposed proof can depend on a property absent from the conjecture. Conversely, a failed conjecture can reveal a useful operation or a stronger question.

The difficulty is to extract a relation that can be investigated generally. Changing a number produces another instance; changing the construction law, allowed maps or quantifier can create a new problem. The latter change needs a mathematical reason and a feasible first attack.

MATH.23:3 - Forces

MATH.23:4 - Solution

Local mantra: recover the construction and its use; vary a consequential ingredient; express the suggested law; seek its reason and a separating case; revise the assertion or construction; choose and begin the next useful problem.

MATH.23:4.1 - Recover what makes the starting construction work

Write the inputs and the operations that produce the result. Identify a relation the result satisfies and where that relation is used. Separate what has been proved from what has only occurred in inspected cases.

Look inside the operation. Repeated updates may expose a recurrence. Combining two constructions may expose closure or an order dependence. A successful quotient may reveal which distinctions can be discarded. MATH.17 helps make the operations themselves available for this investigation.

When a program supplies examples, recover the class it actually generates. For instance, a generator that produces only trees cannot investigate a claim about arbitrary graphs unless the missing graph classes are handled elsewhere. The representation and evaluator are part of the available mathematical experiment.

MATH.23:4.2 - Construct a variation with a reason

Choose an ingredient whose change could affect the wanted relation. Useful mathematical moves include:

These are possible operations, not required stages. Choose the one selected by the construction. MATH.8/.11/.13 supplies symmetry or invariant reasoning; MATH.18 supplies interpretations; MATH.22 develops changed assumptions. Use their fuller methods when that mathematical contribution is needed.

Keep the original use visible. Requiring equal-sized groups repairs a mean-of-means formula, but leaves a request about arbitrary groups unanswered. The latter needs another construction, as in :5.2.

MATH.23:4.3 - State the proposed law and its answer form

Give the objects, domains, allowed operations, assumptions and proposed conclusion. In particular, make the quantifiers distinguishable. These statements ask different questions:

• For each input, some construction has the property.
• One construction works for every input.
• Every admitted construction has the property.

A finite pattern of results can suggest a formula. Derive it from the generating operation, a recurrence, an invariant or another mathematical relation when possible. If that derivation is missing, retain the formula as a conjecture and identify the step that would establish it.

Say what would resolve the present question. An explicit construction, a characterization of all admissible cases, a bound, or a counterexample can open different next uses. A conjectured optimal construction needs both an attainable value and an argument excluding better ones when optimality is the required conclusion.

Check whether the proposed law is already a known result under another description. MATH.18 can compare representations. An available theorem can close this question and expose a more useful next one.

MATH.23:4.4 - Alternate a proof attempt with revealing cases

Use MATH.19 to find intermediate claims connecting the construction to the proposed conclusion. Identify which mathematical property each step consumes. This can expose a condition that the conjecture has not yet stated.

At an uncertain step, construct a case that challenges that condition. Prefer one that distinguishes plausible accounts. To test whether a summary supports composition, find inputs with the same summary and place them in the same surrounding construction. If their required outputs differ, the summary has lost information that composition needs.

Inspect the status of a failure. A counterexample satisfying the conjecture’s premises refutes the conjecture. A failure of an auxiliary lemma may leave a different proof possible. A failed program may instead concern its representation or implementation. Recover the mathematical obstruction before revising the claim.

Computational search can propose constructions and counterexamples. Check a returned candidate against the mathematical conditions that its use requires. For a finite explicit object, this may be a small complete calculation. Sampled tests of an infinite family leave its universal claim to be justified.

MATH.23:4.5 - Revise the claim without hiding the lost use

Use the failure to choose the next mathematical change. Three common returns are:

1. Repair a hypothesis. State the condition that makes the failed lemma work, prove its sufficiency and check whether the intended cases satisfy it.
2. Repair the construction. Retain the original problem and change the objects, representation or operation so that the required property can be obtained.
3. Change the conclusion. Obtain a conditional answer, bound, obstruction or weaker property that still serves a useful question.

A sufficient condition can be worth developing before necessity is known. Label that difference: a proof that uniform convergence preserves continuity does not show that every continuous limit was obtained uniformly.

A counterexample can itself become a constructive ingredient. Ask what class it belongs to, which transformations preserve its obstruction, and which related conjectures it can test. The new question can concern the method of generating cases as well as the cases themselves.

Retain the result that survived. Changing the theorem should not erase a valid construction or an earlier unresolved requirement.

MATH.23:4.6 - Choose a next problem and begin its mathematical work

Compare the few continuations whose answers would change further work. A useful result can supply a missing lemma, a reusable combining operation, an explanation of failure, or a method that makes another class of questions approachable. Immediate engineering application is one possible use; developing a new mathematical operation can also enable later inquiry whose destination is not yet known.

Choose a first attempt that the available contributors can perform. For a broad characterization, this might be one direction of the theorem. For an extremal problem, it might be one explicit improved construction or a bound. For a limit question, it might be the estimate needed to justify one passage to the limit.

Return the conjecture, the mathematical basis that suggested it, the most revealing success or obstruction, and the next operation. An expression and a short argument can carry this result.

Use B.5.QD and C.40.CD when several questions and ways must develop together. E.10.INT helps distinguish the interest of further possible work from surprise, fame or a search score. C.36.RP supplies retention of the reconstructible method when continuing capability is at stake. Obtain further observations or checking only when their possible outcomes can change the next move enough to justify the effort.

MATH.23:5 - Archetypal Grounding

MATH.23:5.1 - From repeated instances to a family of operations

Repeatedly apply f(x)=a*x+b over real numbers. A few calculations give:

f²(x)=a²*x+(a+1)*b,

f³(x)=a³*x+(a²+a+1)*b.

The useful next question is how to represent any number of repetitions without expanding every substitution. The conjectured formula is:

f^n(x)=a^n*x+b*S_n, where S_0=0 and S_n=1+a+...+a^(n-1) for n>0.

Recover the generating rule. Applying f once more changes the coefficient of x from a^n to a^(n+1), and the constant from b*S_n to b*(a*S_n+1). The identity S_(n+1)=a*S_n+1 therefore supplies the induction step. At n=0, f^0 is the identity and S_0=0. The formula is proved for every natural n.

Now vary the problem: combine two potentially different maps f(x)=a*x+b and g(x)=c*x+d. Their composite is:

f(g(x))=(a*c)*x+(a*d+b).

This constructs an operation on coefficient pairs: (a,b) composed with (c,d) gives (a*c,a*d+b). The class is closed under composition. MATH.17 can study this operation; a computational method can use it to combine repetitions.

Order now becomes a useful question. Reversing the maps gives the same linear coefficient but constant c*b+d. Thus they commute exactly when d*(a-1)=b*(c-1). This condition says when reordered operations retain the result.

The progression has produced a general iteration formula, a closed combining operation and a condition for rearrangement. A further question about vector-valued affine maps needs its matrix composition law; scalar commutation cannot be silently carried into that new setting.

MATH.23:5.2 - A failed combination produces a better summary and another conjecture

A computation stores the arithmetic mean of each nonempty group of real numbers. The proposed combining operation takes the mean of those means. For groups [0] and [2,4], it returns (0+3)/2=1.5, while the combined group has mean 2.

Inspect the missing mathematical relation. Each group mean gives a total only when its group size is known. Equal group sizes make the proposed operation work, but arbitrary groups require another construction.

Retain a sum s and count n. Combine (s,n) and (t,m) as (s+t,n+m), then return (s+t)/(n+m) when n+m>0. Associativity and commutativity follow from those of addition in both coordinates; (0,0) is an identity. Thus grouping and order of the combination do not change the final mean in real arithmetic. A finite-precision implementation needs its own error account.

The construction opens a broader mathematical question: Which summaries permit the summary of a combined input to be computed from the two summaries alone?

Let q map a collection of finite lists, closed under concatenation, to proposed summaries; let ++ concatenate lists. Means and medians here use nonempty lists, while sum and count also admit the empty list. A necessary condition is:

if q(u)=q(u’) and q(v)=q(v’), then q(u++v)=q(u’++v’).

It is also sufficient for defining a combining operation on attained summaries: choose lists representing the two summaries and apply q to their concatenation. The condition makes the result independent of those choices. This proves mathematical existence of the operation. Computing it from a concrete representation of the summaries still needs an effective rule. MATH.2 develops the compatible identification; MATH.12 and CMP handle obtaining the operation.

For means alone, take u=[0], u’=[0,0], and v=v’=[6]. The input summaries match, but the concatenated means are 3 and 2. The necessary condition fails. Sum and count repair it by an explicit operation.

Now ask whether median and count suffice. Take u=[0,1,100] and u’=[-100,1,2]. Each has count 3 and median 1. Append the same list [50,50]. The resulting five-element medians are respectively 50 and 2. This new conjecture is refuted by the same method.

The next useful problem concerns what more to retain. Sorted full lists are sufficient and can be merged, while a use requiring less storage can ask for a restricted input class or an approximate median with a stated error. The mathematical obstruction now informs a computational and modeling choice.

MATH.23:5.3 - A failed limit argument reveals a stronger condition

Consider the claim that a pointwise limit of continuous real functions is continuous. On [0,1], let f_n(x)=x^n for positive natural n. Each function is continuous. At any fixed x<1, x^n tends to zero; at x=1 it equals one. The limit f is zero below one and equals one at one, so it is discontinuous.

Locate the failed proof step. Pointwise convergence lets the approximation index depend on x. Continuity near a point needs control over nearby x together. Choosing a good approximation at the one point alone does not control its neighborhood.

This suggests a sufficient condition: uniform convergence. For every positive error allowance, one index makes all later approximations close to f at every point of the domain.

Work the proposed repair. Fix a point x0 and an error allowance e>0. Choose N so that the approximation error between f_N and f is less than e/3 everywhere. Continuity of f_N gives a neighborhood of x0 in which the difference between f_N(x) and f_N(x0) is less than e/3. The triangle inequality bounds the difference between f(x) and f(x0) by these three errors, hence by e. This proves continuity of f at x0.

The repaired theorem supplies a condition for transferring continuity. Here proof analysis discovered which quantifier change made the desired inference possible. A subsequent limit construction can use the proved condition to retain continuity.

Uniformity is sufficient, not necessary. On the domain [0,1), the same x^n sequence has the continuous limit zero, but convergence is not uniform: for every n there is an x<1 with x^n=1/2. The next question can therefore seek a weaker condition suited to the receiving use, rather than treating uniform convergence as the definition of every acceptable limit.

MATH.23:6 - Bias-Annotation

Small examples are chosen to expose a relation and permit a full calculation. In a larger inquiry, simple generators can miss structures with different behavior. Change the generating rule or inspect a contrasting class when that difference could defeat the proposed claim.

A solved or famous problem can attract attention while its reusable mathematical contribution remains unclear. Recover the construction and the questions it opens. The choice of a next problem depends on the work and contributors, not on a universal ranking of interesting statements.

MATH.23:7 - Conformance Checklist

For the conjecture being developed:

• The starting construction, established result and receiving use are recoverable.
• A mathematical change explains why the new question arises.
• Objects, domains, hypotheses, quantifiers and answer form distinguish the proposed claim.
• A proof attempt exposes its needed intermediate relation, and the chosen case tests a consequential condition.
• A counterexample is classified at the claim, lemma or implementation it actually defeats.
• A repaired hypothesis, construction or conclusion preserves the distinction between the new question and any earlier unsatisfied need.
• Generality follows from an argument over the stated class; tested cases retain their actual scope.
• The selected continuation has a useful attainable first operation and retains the earlier construction needed to perform it.

MATH.23:8 - Common Anti-Patterns and How to Avoid Them

Extrapolating the displayed values without the generating law. The iteration formula in :5.1 is justified by its recurrence and induction. Agreement at a few n values alone would leave other continuations possible.

Excluding the counterexample and abandoning the required class. Equal-sized groups rescue the mean-of-means formula in :5.2, but not a requirement to combine arbitrary groups. Sum and count answer that requirement.

Treating a convenient condition as necessary. Uniform convergence repairs the continuity argument in :5.3. The final countercase shows why necessity remains a different claim.

Losing the operation behind a successful answer. Keeping only the mean hides the combining structure. Retaining sum and count makes later aggregation possible; retaining the compatibility argument supports the next summary question.

MATH.23:9 - Consequences

A result becomes material for developing another mathematical problem. A failure can yield a condition, a construction or a new object of study. A success can reveal a family of operations and a way to transfer the result.

The method can stop with a well-formed conjecture and first attempt. Completing its proof, obtaining a computational procedure, learning the method and applying it to a physical subject have their own requirements. Keeping the connection to those uses makes partial progress useful without claiming their completion.

MATH.23:10 - Architectural Rationale

B.5.QD locates a consequential next question. The mathematical contribution here is to construct its proposed law: expose composition and closure, change a quantifier, characterize a compatible identification, or isolate a premise through proof analysis. The cases show how these operations produce statements that can be proved or refuted.

MATH.17/.18, MATH.19/.22 and the other mathematical patterns supply the operative constructions. This pattern assembles them around the development of a conjecture. A case can close with a new question, an answer, or a further obstruction; a universal fixed order of research stages would obscure these returns.

A correct answer and a reusable method have related but different uses. Either can be obtained by people or AI agents. Retaining the derivation, allowed transformations and failed conditions permits another prepared contributor to adapt the work and formulate its next problem.

MATH.23:11 - SoTA-Echoing

The working question is how to develop a mathematical conjecture from constructions and their failures, with a useful route into further work.

Adapt proof analysis. Lakatos’s Proofs and Refutations, Appendix 1 connects counterexamples to the hidden lemmas and concepts in an attempted proof. The adopted move changes :4.4-.5: inspect the failed inference and consider a revised condition or construction. It improves on simply excluding the offending example when that exclusion abandons the intended class. The method can require more work than proving a fixed, adequate claim; use the latter route when its premises and conclusion already serve the inquiry. Lakatos supplies a method for developing the conjecture; its use can still leave the conjecture unresolved.

Adapt construction search and generalization. Georgiev, Gómez-Serrano, Tao and Wagner’s Mathematical exploration and discovery at scale, §§1.3-1.6 and 4 distinguishes search for constructions from finding a program or formula that generalizes, and describes transitions to proof. It also reports evaluator defects and the limits of the tested search methods. This informs :4.1/:4.3-.4: inspect the generator and evaluator, recover a general construction, then establish the claim its use needs. Compared with direct object search, program search can retain reusable structure but adds generation and evaluation cost. A cheap direct search or existing theorem can be preferable. The paper supports these bounded choices, not a universal preference for AI search.

Retain methods as a usable result. The Math and AI declaration of 11 September 2026 argues that counting solved problems can obscure understanding and transmission of methods. Adopt that question in :4.6 and the relation to C.36.RP: preserve what another prepared contributor needs to change and use the construction. The declaration is a position on the purpose of mathematical work, not evidence that transmission must remain exclusively human. The construction-to-proof account above supplies a concrete alternative involving AI contributors.

Reopen the route when a new counterexample changes the admitted class, another representation makes the conjecture simpler, or the receiver needs a result the present construction cannot provide. Improved search tools change the means and cost of investigation; they leave the proposed mathematical assertion and its possible use to be stated.

MATH.23:12 - Relations

• B.5.QD and C.40.CD develop questions and obtaining ways across practices; this pattern supplies the mathematical conjecture-forming contribution.
• MATH.17/.18 supply operations on constructions and interpretations between accounts.
• MATH.8/.9/.11/.13 supply symmetry, selection and invariant methods that reveal general relations or obstructions.
• MATH.19/.6/.22 supply proof construction, countermodels and changed axioms.
• MATH.2 supplies the compatible identification used by composable summaries.
• C.29 and MMP interpret the mathematical result for a subject; CMP supplies effective search, construction and execution when needed.
• E.10.INT, C.36.RP and HCD and Core opportunity construction support interest, continuing availability of methods and acquisition of a missing capability.

MATH.23:End