Part B - Construct and criticize arguments

MATH.19 - Construct a Proof through Intermediate Claims

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

MATH.19:1 - Problem frame

Use this pattern when you have a mathematical claim to establish and some relevant definitions or results, but no argument connecting them. A calculation may suggest the answer while leaving its generality unexplained. An induction step may need information that its hypothesis does not provide. A familiar theorem may almost fit, with one missing premise.

Construct intermediate claims that connect what is available to what is required. A lemma is an auxiliary proved claim used in another argument. Finding a useful lemma is part of the work: its conclusion must help the next step, and its premises must be obtainable where it is used.

First useful move: unfold the wanted conclusion once. Ask what would suffice to establish it, and which available statement or construction could supply that condition. Try to complete this connection on an arbitrary admitted object.

The reader needs elementary mathematical statements, functions and the idea of a proof from assumptions. The worked cases explain their additional notation. The method supports arguments about numbers, functions, structures and mathematical models; each branch retains its own assumptions.

Use a supplied theorem directly when its premises are met and its conclusion answers the question. B.5.RA helps recover an existing unfamiliar argument. MATH.4 develops the inductive construction when induction is the required step; MATH.12 recovers an obtaining procedure from a proof. Here the missing contribution is the proof’s construction and organization.

MATH.19:2 - Problem

Forward calculation can produce true statements without approaching the wanted conclusion. Working backward can produce a useful-looking requirement that is stronger than the available assumptions. Combining the two requires discovering a statement that is both obtainable and sufficient for the next inference.

The difficulty can be hidden in a parameter or an order of composition. A proof for one selected object may be used as if it covered all objects; an auxiliary claim may quietly assume the theorem being proved. A recursive step can demand a result for a changed parameter even though the induction hypothesis fixes it.

The needed result is an argument with its assumptions and connections recoverable. If it cannot yet be completed, identify the remaining mathematical claim and what proving or refuting it would enable.

MATH.19:3 - Forces

MATH.19:4 - Solution

Local mantra: recover the claim; work backward from what would suffice; work forward from what is available; construct the connecting lemma; complete the argument; use it or revise the remaining question.

MATH.19:4.1 - State the claim at the scope its use needs

Identify the objects, assumptions and required conclusion. Unfold a definition when doing so exposes the operation the proof needs. For injectivity of f, the task becomes: for arbitrary a and b in its domain, derive a=b from f(a)=f(b).

Keep track of which parameters are fixed and which may vary. A claim for every input requires reasoning that covers every admitted input. A temporary assumption belongs to the implication or case in which it was introduced.

Choose the kind of conclusion needed. Proving existence, obtaining a particular object and supplying a uniform effective procedure can require different contributions. MATH.12 handles extraction when the proof is expected to yield data; CMP supplies execution and cost methods when those become the next question.

When the intended statement is still unclear, first recover or change it with B.5.FM or B.5.RA. Proof construction can begin with an informal mathematical statement whose objects and inferential obligations are clear.

MATH.19:4.2 - Work backward to sufficient claims

Inspect how the conclusion could be established. Common entry moves include:

An established theorem can replace one target with several premise obligations. A proposed lemma can do the same, but remains an obligation until proved. Retain why the proposed premises would suffice: this is the connection that makes the lemma useful.

Some backward moves deliberately strengthen the task. To show that two complicated expressions have the same value, finding one common normal form may be convenient. If the stronger task becomes obstructed, return to the weaker conclusion or find another route.

MATH.19:4.3 - Work forward and construct the connecting lemma

From the available definitions, equations, hypotheses or objects, derive consequences likely to supply an open obligation. Apply a function to an established equality; construct an element that a definition requires; substitute a known relation; or separate cases when they give different available facts.

Compare the expressions produced with the expressions needed. Their difference often identifies the lemma: an operation must commute past a repeated operation, an equality must survive a map, or a parameter must be allowed to vary. State that relation with all operands and hypotheses.

Then ask two questions together: can the lemma be established from what is available, and does it actually complete the next inference? Test the proposed statement on a small revealing case before investing in a long argument when such a case could defeat it. MATH.6 constructs a countermodel when a false intermediary is suspected.

Use the simplest sufficient connection. If substitution and a supplied identity finish the argument, no separate named lemma is needed. If several later steps need the same derived fact, prove it once and use it with its conditions.

When an auxiliary claim asks for more than the next inference needs, try a weaker conclusion that still closes that inference. Keep the original theorem fixed, prove the weaker lemma, and check its use in the argument. For a limit argument, a bound valid from some index onward may suffice even when the same bound on every term is false.

MATH.19:4.4 - Change the carried claim when a step needs more

At a stalled step, inspect what it actually consumes. It may need the claim for a different parameter, an additional retained quantity, or all smaller inputs instead of only the immediate predecessor.

Strengthen or generalize the carried claim to supply that information, then recheck its starting cases and every affected step. MATH.4 develops the corresponding inductive constructor and property proof. A stronger hypothesis inside an induction argument must come from the chosen induction principle and its proved cases.

Adding a new premise is a different repair. It narrows the theorem’s applicability. Check whether the receiving problem supplies that premise; otherwise the revised theorem answers a changed question. The changed commutation condition in :5.2 demonstrates this boundary.

The argument may also need a different representation. MATH.17 supplies operations on operations, and MATH.18 compares interpretations when that change can make the missing mathematical relation available.

MATH.19:4.5 - Assemble the argument and inspect its dependencies

Order the proved claims so that each step uses available results. State an auxiliary lemma with the hypotheses under which it was proved, then bind its variables to the objects of the receiving step.

Inspect any apparent cycle. Induction can justify use of a smaller case under its decrease condition; it cannot justify using the current theorem as an unproved premise of its own auxiliary lemma. Separate the required earlier result or change the argument.

For cases, establish the target for every admitted branch. For an implication, discharge its temporary assumption when returning to the outer argument. For a contradiction argument, retain the logical principle that turns the contradiction into the requested conclusion; extracting a witness can remain a further question.

Write enough of the completed argument for another prepared reader to recover the decisive inference. A proof assistant can check a formal derivation and its dependencies when that is useful. Compare the checked statement with the intended statement before using the result.

MATH.19:4.6 - Return the result to its use

A completed proof supplies its conclusion under the stated assumptions. Use that result in the next mathematical construction, model argument or algorithmic design. When a changed premise invalidates a lemma, reopen its dependent steps and retain arguments that still apply.

An incomplete proof plan can still locate useful work: name the remaining lemma, its available premises, and the step it would close. This can support another reader, a specialist or an AI agent without concealing the open part. If a counterexample defeats the claim, return it and the failed premise or implication.

An obstruction can also motivate changing an axiom or developing a conjecture. Carry the failed relation and the intended use into that new mathematical question.

MATH.19:5 - Archetypal Grounding

MATH.19:5.1 - Choose the intermediate equality that proves injectivity

Let f:A->B and g:B->A satisfy g(f(a))=a for every a in A. Prove that f is injective.

Work backward from injectivity: choose arbitrary a,b in A and assume f(a)=f(b). The required conclusion is a=b. The given identity involves g(f(a)), so work forward by applying g to the assumed equality:

g(f(a))=g(f(b)).

Substitute the two given identities to obtain a=b. The intermediate equality connects the assumption to the goal; no larger theory is needed.

Now replace the given identity by f(g(b))=b for every b in B. The same proof cannot simplify g(f(a)). What it does supply is surjectivity of f: for an arbitrary b, choose a=g(b), then f(a)=b.

For a concrete separating case, take A={0,1}, B={*}, f(0)=f(1)=*, and g(*)=0. The changed identity holds, but f is not injective. The failure identifies which composite was required and produces the useful conclusion that remains. MATH.18 can use these two composites when comparing descriptions.

MATH.19:5.2 - Discover the lemma needed to repeat a composition

Let f and g be maps X->X with f composed with g equal to g composed with f. Write composition as juxtaposition, with fg meaning apply g first and then f. Define f^0=id and f^(n+1)=f^n f, and similarly for g. Prove:

(fg)^n=f^n g^n

for every natural n.

The base n=0 holds. At the next step, the proposed induction hypothesis gives:

(fg)^(n+1)=f^n g^n f g.

The target is f^(n+1)g^(n+1). The difference exposes a missing lemma: g^n f=f g^n. This states precisely how to move f past the repeated g.

Prove that lemma by induction. At n=0 both sides are f. If it holds at n, then:

g^(n+1)f=g^n g f=g^n f g=f g^n g=f g^(n+1).

The second equality uses gf=fg; the third uses the lemma’s induction hypothesis. Return to the original step:

f^n g^n f g=f^n f g^n g=f^(n+1)g^(n+1).

The two inductions now have separate proved responsibilities. MATH.4 supplies their general induction method; the present work found which additional statement makes the main step possible.

Remove the commutation premise. On integers, f(x)=x+1 and g(x)=2x give (fg)^2(0)=3, while f^2 g^2(0)=2. The theorem has become false. Retaining the premise or retaining the actual interleaved composition are different useful responses; continuing the old rearrangement would lose the result needed by the calculation.

MATH.19:5.3 - Generalize a parameter to make the proof close

Suppose a finite list is built as [] or x::xs. Define append ++ in the usual way, with []++a=a and (x::xs)++a=x::(xs++a). Let [x] denote the one-element list.

Define reversal by R([])=[] and R(x::xs)=R(xs)++[x]. A second construction carries an accumulator:

T([],a)=a,

T(x::xs,a)=T(xs,x::a).

The wanted result is T(xs,[])=R(xs). Induction on xs with only this statement stalls: the recursive call uses accumulator x::[], while the hypothesis concerns [].

Generalize to every accumulator a:

T(xs,a)=R(xs)++a.

The empty-list case gives a=[]++a. For a nonempty list, the generalized induction hypothesis gives:

T(x::xs,a)=T(xs,x::a)=R(xs)++(x::a).

Using x::a=[x]++a and associativity of append, this equals (R(xs)++[x])++a=R(x::xs)++a. Append associativity itself follows by induction on its first list: the empty case is the defining rule, and the nonempty case reduces after the common leading element to the induction hypothesis.

Setting a=[] recovers the original target, using append’s right-identity law. That law also follows from the same two formation cases. On [1,2,3], the accumulator states [], [1], [2,1], [3,2,1] make the changed parameter visible.

The proof establishes equality of the two list results. A claim that one implementation uses less time or storage additionally depends on its list representation and execution model. Those are computational questions for the obtained construction.

MATH.19:6 - Bias-Annotation

A short final proof can hide the search that found its auxiliary claim. When helping another reader construct a proof, expose the expression or missing premise that motivated the lemma, as in :5.2.

Successful instances can guide that search. The universal conclusion still needs an argument covering its admitted objects; the noncommuting maps in :5.2 show why one successful calculation could miss the decisive premise.

MATH.19:7 - Conformance Checklist

For the argument being constructed:

• The objects, variable scope, assumptions and wanted conclusion are recoverable.
• Each backward obligation has a stated implication to the claim it is meant to establish.
• Each reused or newly proved lemma has its premises satisfied at the point of use.
• A strengthened induction claim supplies the actual changed parameter or retained information, with its starting cases and step rechecked.
• Every admitted case is covered, and circular dependence is discharged by a valid argument such as induction.
• The final statement is the one the mathematical work needs; any additional applicability condition is visible.
• The result is a completed argument, a counterexample, or a particular remaining mathematical obligation with a useful continuation.

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

Using the desired conclusion inside its supporting lemma. If the lemma that justifies a rearrangement is proved by assuming that rearrangement, the gap remains. Prove the smaller commuting statement from its own premise, as in :5.2.

Fixing a parameter that the next step changes. The empty-accumulator hypothesis in :5.3 cannot be applied to a nonempty accumulator. Generalize the statement and recheck the base and step.

Silently changing a premise to finish the proof. Commutation makes the rearrangement in :5.2 valid. If it is absent from the intended use, state the changed theorem or retain the interleaved operation.

Closing a different composite. The two inverse identities in :5.1 support different conclusions. Compare the operands and order of the proved statement with the question being answered.

MATH.19:9 - Consequences

Proof construction becomes work on smaller mathematical claims with visible dependencies. The remaining difficulty can be assigned or investigated without requiring another agent to reconstruct the entire search.

A successful argument can reveal a more reusable lemma, a changed theorem or a new construction. When the claim fails, the separating case can guide the next problem. The resulting generality follows from the proved assumptions and operations.

MATH.19:10 - Architectural Rationale

Backward obligations expose what would suffice; forward constructions expose what can be obtained. A useful intermediate claim joins the two. This organization supports informal reasoning and formal derivations while preserving the mathematical question as the governing object.

Induction, countermodels, interpretation and witness extraction contribute different operations. The stalled inference determines which contribution the argument needs: the list example requires a varying parameter, while the composition example requires a separately proved commutation relation.

The proof plan and its completion have different uses. A plan can locate a lemma for a collaborator; a completed argument supports the mathematical conclusion. Making that distinction visible permits useful incomplete work without treating the remaining obligation as already solved.

MATH.19:11 - SoTA-Echoing

The working question is how to construct a missing mathematical argument from available objects, assumptions and results. The selected approach combines backward proof obligations with forward derivation, then changes an intermediary or the carried claim when their connection fails.

Avigad, Lewis and van Doorn’s Logic and Proof, §3.3 gives an explicit account of the two reasoning directions and hypothesis scope. The current Theorem Proving in Lean 4, Tactics shows how applying a result creates premise goals and how local intermediate claims organize a derivation. Here those contributions inform :4.1-.3/:4.5; using Lean is optional.

Tao’s mathematical research advice connects progress at lemma scale with the larger problem and recommends changing the point of attack when present methods are insufficient. The pattern gives that move concrete form through a failed intermediate claim and its revised continuation. This source is methodological advice, not a completeness guarantee for proof search.

A direct calculation or an already applicable theorem is preferable when it settles the claim with less effort. Unstructured forward manipulation becomes a poor alternative when it leaves the target unchanged; a single backward chain becomes a poor alternative when its generated premise cannot be obtained. The adopted combination changes :4.2-.4, as the missing commutation lemma and accumulator generalization demonstrate.

The sources provide construction methods and inspectable formal mechanisms. They do not make the proposed heuristic complete for all mathematical theories. Reopen the chosen proof route when a premise changes, a lemma fails, a better theorem or representation becomes available, or the receiver needs a constructive output or execution property not yet supplied.

MATH.19:12 - Relations

• B.5.RA recovers an existing argument for its next use; B.5.FM helps formulate an unresolved question.
• MATH.4 constructs and justifies inductive operations, including strengthened parameters.
• MATH.6 develops a countermodel when an intermediate or final claim may be false.
• MATH.12 extracts the construction an argument supplies.
• MATH.17/.18 develop operations on operations and interpretations used by a proof.
• C.29 connects a mathematical result to its modeled subject. Computational realization and cost remain with the corresponding CMP methods.
• B.5.QD and C.40.CD develop the next useful question when the argument or obstruction opens one.

MATH.19:End

MATH.4 - Construct a Witness by Induction

Type: Method Status: Stable Normativity: Normative

MATH.4:1 - Problem frame

Use this pattern when an input is given as a finite construction from smaller inputs, and you need a way to produce an object with a required property for every such input. You may know the desired equation or have an existence argument, while the operation that obtains an answer remains missing.

A witness is the object that satisfies the requirement: a quotient and remainder, for example, or a coloring with a stated property. Construct a witness for each base case, then construct one for a larger input from the witnesses for its immediate constituents. The same case structure gives a reason why the result has the required property.

Start with the smallest input and one step that builds the next input. Return a base witness and a usable step, or identify what the step still cannot construct. You need functions, elementary logical conditions and the input’s formation rules. The number example also uses integer arithmetic; the tree example explains its own constructors.

This method starts with freely formed constructor expressions: each input supplies its outermost constructor and its constituent inputs. When different expressions represent the same object, section 4.4 explains the additional step needed for a function of that object. If a supplied operation already returns the required object, use it. An existence result can also be sufficient when no witness or way of producing one is needed. Infinite behavior or a recursion that does not follow smaller constituents needs a different termination or continuation argument.

MATH.4:2 - Problem

An assertion that a suitable object exists can leave the receiver unable to obtain it. A recursive formula can leave a different gap: it may call itself without reaching an answer, omit a case, or return objects that fail the required property.

The mathematical task is to build the operation and its justification together. The case for a larger input must use only what the smaller-input results actually provide. Sometimes this reveals that the proposed result was too weak: the step needs an extra parameter or an auxiliary value.

MATH.4:3 - Forces

MATH.4:4 - Solution

Local mantra: state the wanted object; build the base; build the next case from smaller cases; justify the construction; use the witness.

MATH.4:4.1 - State the input construction and wanted result

Name the input family, its constructors and any fixed parameters. For natural numbers, the constructors are zero and successor. A finite binary tree can be a leaf or a new root joining two smaller trees. The supplied constructor and constituents determine which recursive clause applies. If different constructions are later identified, retain that identification as a separate condition.

For each input x, state the kind of output y and the property P(x,y) it must satisfy. Include bounds or retained information that the next use consumes. For division by a positive integer d, the output is a pair (q,r) satisfying n=q*d+r and 0≤r<d.

Use the input’s actual formation rules to choose the cases. A proof about trees cannot be applied to a structure with additional edges without considering those edges.

MATH.4:4.2 - Construct the base witnesses

For each constructor with no smaller inputs, give an output and show that it satisfies the required property. This supplies the point at which recursive evaluation can return a value.

If the base fails, inspect the specification or its parameter conditions. Do not invent a default output that fails the requirement merely to complete the cases.

MATH.4:4.3 - Construct the step and strengthen what it needs

Take one constructor with smaller inputs. Assume that each smaller input already has an output satisfying the stated property. Give an operation that uses those outputs to build the required output for the whole input.

Show why the construction preserves the property. Check each branch that changes the returned object. When the step needs information absent from the proposed output, strengthen the result or generalize a fixed parameter, then revisit the base cases and affected steps.

For example, a tree-coloring step may need to choose either color for a subtree’s root. A construction that promises only a root of color zero leaves that step unsupported. A construction parameterized by the required root color supplies what the step uses.

To obtain an executable construction, each case distinction must be decidable from the supplied data, and each operation used to build an output must itself return. A step that says only “choose a suitable object” identifies further mathematical work unless a way to make that choice is already supplied.

MATH.4:4.4 - Define the operation and establish its result

For a natural-number input, let b be the base witness and let step(n,y) produce a witness for n+1 from one for n. Define:

F(0)=b

F(n+1)=step(n,F(n)).

The base argument establishes P(0,F(0)). The step argument establishes P(n+1,F(n+1)) from P(n,F(n)). Induction therefore establishes the property for every natural number.

For another finite inductive input, give one defining clause and one property argument per constructor. Recursive calls use its immediate constituents. Evaluation terminates because these calls descend through a finite input construction, provided the operations within each clause terminate.

When different constructor expressions represent one object, the recursion first gives a function of expressions. To obtain a function of the represented object, establish that all its permitted expressions yield the same required output, using MATH.2. Alternatively, supply an additional rule that chooses one construction from the object. Keeping the construction as part of the input is also useful when its history matters.

For example, build a finite set with Empty and Insert(a,S) for a outside S. Returning [] at the base and prepending a at each step gives a list containing each element once. Yet Insert(1,Insert(2,Empty)) and Insert(2,Insert(1,Empty)) represent the same set and return [1,2] and [2,1]. Both are valid witnesses, but these clauses define a function of the insertion construction. If a function of the set is required and its elements have a supplied total order, strengthen the output requirement to an increasing list and insert each element in order. The unique increasing list then makes the output independent of insertion order. This repair uses the ordering operation and a stronger specification.

A dependent-type description can package the output with a proof of its property. Its first projection returns the witness; the other component justifies that witness for the stated input. An ordinary mathematical presentation may instead give the function and proof separately. Use the presentation needed for the receiving work.

MATH.4:4.5 - Use the witness and return after a changed requirement

Evaluate the construction for the needed input. Return the object and the property on which its next use relies. Reuse the general argument while its constructors, clauses and premises remain unchanged.

If the receiver needs another quantity, check whether the current result retains it. If a parameter or formation rule changes, return to the affected base or constructor clause. If constructions are newly identified, check whether the output still defines a function on those identified inputs. A failed clause can supply a counterexample or a more specific construction question.

An executable recursive construction is already an algorithm. Its operation count, storage and representation can become further design questions when the intended scale makes them matter. A faster implementation can retain the same mathematical specification; the correspondence between the two constructions needs its own argument.

Stop with the required witness, a reusable construction with its property, or a particular unresolved clause. Formalizing the same result in a proof assistant is useful when that receiving use needs it.

MATH.4:5 - Archetypal Grounding

MATH.4:5.1 - Obtain quotient and remainder together

Given a natural number n and a fixed positive integer d, construct natural numbers q,r such that n=q*d+r and 0≤r<d.

At n=0, return (0,0). The equation holds, and positivity of d gives the remainder bound.

Suppose the result for n is (q,r). To obtain the result for n+1:

• if r+1<d, return (q,r+1);
• otherwise return (q+1,0).

Because r<d and the values are integers, the second branch has r+1=d. In the first branch, n+1=q*d+(r+1); in the second, n+1=(q+1)*d+0. Both branches preserve the required bound. This proves the recursive construction for all natural-number inputs.

For d=3, successive witnesses include:

The output for 8 determines both two completed groups of three and a remainder of two. Keeping only the remainder would lose the number of completed groups. MATH.2 explains which questions such a reduced result can still answer.

The construction takes one successor step per unit of n. It exposes the witness and proof economically as mathematics, but a large encoded integer can call for a different division algorithm. If division with the same convention is already supplied, use that operation.

Changing the parameter to d=0 defeats the specification: no natural r satisfies 0≤r<0. This returns a failed input condition before any recursive step. Extending the input to negative integers also requires a new case; the natural-number recursion does not cover that extension.

MATH.4:5.2 - Strengthen the construction to color a tree

Consider finite binary trees formed as Leaf or Branch(left,right). A leaf is one vertex. A branch adds a new root with edges to the roots of its two constituent trees. The constituent vertices occur separately in the constructed tree.

The required output colors each vertex 0 or 1 so that each edge joins different colors. Suppose a first attempt always colors a root zero. At a new branch, using those subtree results unchanged would give edges from zero to zero.

Generalize the construction: Color(t,c) takes a tree and a required root color c∈{0,1}. Its result must have root color c and different colors across every edge.

• For Leaf, return its single vertex with color c.
• For Branch(left,right), color the new root c, and use Color(left,1-c) and Color(right,1-c) for its constituent trees.

The leaf has no edge to violate the property. At a branch, the induction hypotheses supply the property within each constituent tree. Their roots have color 1-c, so both new edges also join different colors. The construction therefore satisfies the specification for both choices of c.

For Branch(Leaf,Branch(Leaf,Leaf)) with root color 0, the two children receive color 1 and the two grandchildren receive color 0. The strengthened parameter made the recursive step possible.

Now add edges beyond the tree construction. On a triangle, choosing colors 0 and 1 for two adjacent vertices forces the third to be 0 to differ from the second, but it then agrees with the first. The tree result therefore cannot provide the requested coloring for every graph. The new edge condition leads to a different construction or an obstruction, while the tree method retains its original use.

MATH.4:6 - Bias-Annotation

A familiar induction proof can tempt the writer to leave the output operation implicit. Recover the witness produced in each case and the information the next case uses.

A second temptation is to keep the initial statement fixed even after the recursive step exposes missing information. The tree case needs both root colors; strengthening that specification repairs the construction.

Simple recursion can also look like a recommended implementation. The division case states its cost so that a mathematically useful construction can be replaced for a larger computational use.

MATH.4:7 - Conformance Checklist

• Are the input constructors, supplied construction and parameter conditions stated?
• When different constructions represent one object, is any claimed function of that object independent of the construction or supported by a stated selection rule?
• Does each base case return an object satisfying the specification?
• Does every constructor clause use only supplied data and results justified for smaller inputs?
• When an auxiliary value or parameter is needed, do the strengthened specification, base and step agree?
• Are all case distinctions and witness-producing operations available for the claimed executable use?
• Do recursive calls descend through finite constituents, or is another termination argument supplied?
• Can the receiver obtain the witness and recover the property it uses?
• After a changed requirement, is the affected clause or missing construction identified?

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

Prove existence while omitting the requested witness. Recover the producing operation in each case. If the argument supplies no such operation, keep its existence conclusion and return the remaining construction question.

Fill an uncovered case with an arbitrary value. A total expression can still violate the specification. Check the value under the case’s premises or expose the failed condition, as with division by zero.

Use an induction hypothesis too weak for the step. The tree’s fixed-root-color attempt fails at the new edges. Quantify the needed color parameter and establish the stronger base and step.

Recurse on an unchanged input. The finite-constituent argument no longer establishes termination. Change the recursive calls or obtain a different well-founded argument.

Transfer the proof after changing the input’s formation. The extra edge in the triangle is absent from the tree constructors. Reopen that new case before claiming the property for the larger family.

MATH.4:9 - Consequences

The result is a reusable way to obtain witnesses, with a reason for the property each witness satisfies. Construction and justification expose the same case boundaries, making a changed premise easier to locate.

Strengthening the result can add parameters or auxiliary values. Those additions cost representation and calculation but can supply the information that makes the inductive step work.

An efficient implementation remains a further opportunity when the simple construction is too costly.

MATH.4:10 - Architectural Rationale

The input’s formation rules determine the cases. Pairing each output rule with its property argument links object construction, reasoning and computation without requiring a proof-assistant language.

The stronger specification is part of the construction method. It lets a smaller-input result provide what a larger input needs, as the root-color parameter shows. Returning the witness separately from optional proof packaging keeps the result usable in different mathematical and computational descriptions.

Structural recursion was selected because finite constituent structure supplies a local termination argument. Finite enumeration is a serious alternative for one small instance, and an existing operation can be the cheapest way to obtain its answer. Inductive construction earns its extra work when a family, reusable operation or premise-sensitive argument is needed.

The division and tree cases use different objects while sharing the base-and-constructor move.

MATH.4:11 - SoTA-Echoing

Question: how can a specification over inductively formed inputs produce a witness-building operation and a reusable correctness argument?

Adopt the induction and computation rules from Egbert Rijke’s Introduction to Homotopy Type Theory, §3.1, printed pp.19-22. Section 4.6, pp.33-34, supplies dependent pairs and their projections as one formal presentation of an output with dependent information. The pattern uses these construction questions in ordinary mathematical language; it does not require univalent foundations for the examples.

The current Theorem Proving in Lean 4, §8.3 gives an operative comparison: recursive definitions and induction follow the input constructors, with recursive calls on smaller constituent terms. Adapt that organization here by foregrounding the wanted witness and strengthening the result when a step cannot be built. The integer and tree constructions are authored examples of the method.

The book’s axiom-of-choice discussion shows why formal existence and executable witness production require separate attention: definitions that manufacture data through classical choice are noncomputable in that setting. This makes recovering the output rule consequential; classical reasoning about an independently computable operation can still be useful.

Direct enumeration or a supplied operation can answer a small instance with less construction work. Reopen the selected method when the input is no longer finite and inductively formed, a required choice lacks an obtaining operation, or execution cost calls for another algorithm. The set example adds the representative-independence question supplied by MATH.2: producing a witness from each expression and defining one function on identified inputs require different arguments.

MATH.4:12 - Relations

• Uses FPF B.5.RC and B.5.RA when needed: recover an unfamiliar input construction or proof before choosing the cases.
• Connects with MATH.1: a witness can itself be a constructed path; a changed step can alter its permitted joins.
• Uses MATH.2 when input constructions are identified: establish whether the output is independent of their representative. MATH.2 also helps retain the information needed by the next operation when simplifying a witness.
• Connects with FPF B.5.RR and B.5.QD: locate the first failed clause after a changed premise and develop the resulting construction question.
• Connects with FPF C.29 and C.29.2: interpret the mathematical result and relate an executable procedure to its claimed result.
• Connects with algorithm design: compare other constructions, representations and resource use while preserving the needed specification.

MATH.4:End

MATH.12 - Extract a Construction from a Proof

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

MATH.12:1 - Problem frame

Use this pattern when a mathematical proof says that an object can be obtained, but you still need the operation that obtains it. The proof may describe the object through several intermediate results, hide it inside a pair, or use cases whose choice must be made from the input.

Recover the values and operations carried by the argument. A proof that a number is divisible by four can supply the quotient; a proof connecting two function types can supply transformations between their functions. When a step supplies only existence, the same reading identifies the construction still needed.

First useful move: find where the wanted object is introduced. Write the expression for that object and the inputs used to form it. Follow each needed input back to a supplied value, an available operation or a missing construction.

The reader needs functions, pairs, case distinctions and elementary mathematical reasoning. The arithmetic cases use integers and fractions. The function case explains its own notation. Use an already available operation directly when it returns the required object. An existence conclusion can be sufficient when the receiving question does not require obtaining a witness.

This method works through constructive proof steps and their computation rules. A claim about every input needs a construction that can be applied to every input in that scope. Some proofs establish their conclusion without supplying such a construction; :4.4 determines what can still be used from them.

MATH.12:2 - Problem

Knowing that an answer exists can leave the next calculation impossible to perform. Even when a proof contains an answer, its presentation may separate the values needed to compute it or suppress their dependencies.

There is also a possible mismatch between mathematical reasoning and execution. A proof can distinguish two cases without providing a procedure that selects one. A formal system can store an existence proposition in a form that does not expose its witness as program data.

The needed result is an operation with stated inputs and an argument that its output satisfies the requested relation. A missing branch decision, unavailable auxiliary operation or unsupported termination claim is a specific remaining problem.

MATH.12:3 - Forces

MATH.12:4 - Solution

Name the wanted output → recover its construction → compose the supplying steps → check computation → obtain the witness → revise affected dependencies.

MATH.12:4.1 - State what must be obtained

Name the input x, any parameters and the relation R(x,y) required of the output y. A statement “for every x there is a y satisfying R(x,y)” leaves the next task open until the needed y can be supplied.

State what the input actually contains. A value with an associated proof, a procedure returning such a value, and a proposition asserting that some value exists support different operations. For example, a pair (k,p), where p justifies n=4k, supplies k by projection. A statement that n is divisible by four may require recovering or constructing that k.

Keep the order of dependence. The output of “for each x, construct y” may depend on x. It does not thereby supply one y that works for every x.

When the argument is unfamiliar, B.5.RA can recover its premises and deductions before this computational reading.

MATH.12:4.2 - Recover what each proof step supplies

Begin at the desired conclusion and follow the steps needed to produce its object. Give each supplied value a name. For a lemma used along the way, recover the obtaining operation when the next step consumes its output as data.

The following constructions give a small working repertoire:

A constructive disjunction carries which case holds. If the source argument provides no such choice, name the missing decision before turning it into a conditional program.

For an inductive argument, recover the base and constructor operations through MATH.4. That pattern also handles a step that needs a stronger result. The present method assembles the values supplied by those operations with the other proof steps.

MATH.12:4.3 - Compose the operations and simplify their use

Substitute each supplied result into the place that consumes it. Preserve names for inputs whose values differ or whose dependencies matter.

Some simplifications directly expose a wanted value:

• Applying x ↦ t(x) to a gives t with a substituted for x.
• The first component of (b,c) is b; the second is c.
• A case distinction applied to a tagged value runs the branch named by its tag.

These are computation rules for the chosen constructions. Use their conditions, including the input type and any variable binding. Rename an auxiliary variable when substitution would confuse it with another input.

For a proof supplying a dependent pair p(x)=(y,q), define F(x) as its first component. The second component then supplies R(x,F(x)). This gives both an obtaining operation and the relation its output satisfies, provided the construction of p(x) is available.

Write the resulting expression or procedure in a representation the receiver can use. A short formula can be sufficient. Pseudocode or a proof-assistant term is useful when its evaluation or composition is the next question.

MATH.12:4.4 - Determine which computation the argument supports

Inspect every operation on which the returned data depends. Is it supplied? Does it return on the permitted inputs? Can the case distinctions be decided? Finite composition of terminating operations gives an obtaining procedure; recursion needs its stated termination argument.

A proof step that invokes a classical choice of an element does not, by that invocation alone, give an executable choice procedure. Retain the existence result and either obtain a construction for that step or use another proof that supplies one. Classical reasoning can still justify a separately defined computable function.

Suppose a finite list is supplied together with a terminating test P and a proof that some listed element passes. Test the elements in order and return the first that passes. The list makes the search finite, and the proof rules out exhaustion without a result. For [2,5,8] and P(n)=(n>6), this returns 8 after three tests. The existence proof may use classical reasoning: the returned data comes from the search.

For a formalized proof, inspect the system’s actual rules for data and proofs. In Lean, for example, an existential proposition in Prop is not a data-bearing dependent pair whose witness a program may simply project. A value packaged in a data type with a proof of its property can retain its data while compilation erases the proof. Choice used to manufacture the data is a separate computational issue.

The chosen logic and evaluation rules determine the proof-to-computation correspondence. General recursion can describe a computation that never returns; its type alone need not establish the requested terminating construction. An ordinary proof narrative also needs its object-producing steps recovered before it provides that construction.

MATH.12:4.5 - Obtain the result and use its justification

Apply the extracted operation to the input of interest. Follow its reductions far enough to obtain the requested value, and use the proof’s retained relation to justify that value.

A worked input checks that the expression can be followed. The general output claim comes from the construction and its proof under the stated assumptions. Where the representation can overflow, round or reorder dependent updates, establish that its operations preserve the mathematical result needed here.

Retain intermediate results when recomputation would matter. A proof transformation that preserves a function’s output can still duplicate an expensive calculation. Compare implementation choices under the same output requirement.

For work on another subject, use C.29 to establish the correspondence between the mathematical construction and that subject. C.29.3 connects a computation with its input preparation, execution and result interpretation. A mathematical function transformation can inform a change of method while the changed method still needs its physical, resource and interaction conditions.

Stop with the required object, a reusable obtaining operation with its property, or the particular premise that still lacks a construction.

MATH.12:4.6 - Return to the changed dependency

If only the input value changes within the proved scope, apply the same operation. If a premise changes, locate the earliest producing step or branch that uses it.

A stronger output requirement can need an additional value. A changed representation can remove a previously available projection or decision. Reconstruct that part, then follow its effects through the receiving expressions and justification.

When different input descriptions are identified, MATH.2 determines whether the obtained output is independent of the description; MATH.7 can carry it through a reversible representation. B.5.RR follows changed premises through the surrounding argument.

MATH.12:5 - Archetypal Grounding

MATH.12:5.1 - Recover the witness in an arithmetic argument

For integers a,b, a proof shows that (a+b)^2-(a-b)^2 is divisible by four. The receiver wants the quotient.

Expanding the squares gives:

(a+b)^2-(a-b)^2 = 4*a*b.

The existence statement is “there is an integer k such that the difference is 4k.” Its witness-introducing step chooses k=a*b. The extracted operation is therefore multiplication of the two inputs, with the displayed identity as its justification.

At a=3,b=2, the difference is 25-1=24 and the operation returns k=6. The receiver can use 6 without reconstructing the expansion on every input.

Now ask for divisibility by eight. The old proof supplies 4ab, which is insufficient: at a=b=1 the difference is 4. A supplied stronger premise a=2r repairs the construction:

4*a*b = 8*r*b.

The new witness is r*b. If the input already carries r, the procedure uses it. If only an assertion that a is even is supplied, obtain the integer r with a=2r or use an available integer-division operation with its conditions. The changed proof identifies both the new premise and the additional input needed by its expression.

MATH.12:5.2 - Read a function equivalence as two transformations

Suppose f maps each a in A to a pair in B×C. A proof can split this into two functions by projecting its output:

Split(f) = (a ↦ first(f(a)), a ↦ second(f(a))).

Conversely, given g:A→B and h:A→C, pair their values:

Join(g,h) = a ↦ (g(a),h(a)).

Applying Join after Split gives, at each a:

(first(f(a)),second(f(a))) = f(a).

Applying Split after Join returns g and h pointwise. Thus the argument supplies transformations in both directions, together with the equalities that justify using the returned functions.

For f(n)=(n+1,n^2), Split gives g(n)=n+1 and h(n)=n^2. Joining their values at n=3 returns (4,9). The projections and applications are the computational content of the proof.

The equality concerns functions with values determined by their input. If evaluating f is expensive, the expression using two calls can repeat work; calculate f(a) once and keep its pair when both components are needed.

If the proposed implementation instead reads and increments a hidden counter, repeated calls change the situation. A single call returning (c,c) might give (1,1), while separate component calls yield (1,2). This no longer implements the fixed mathematical f used by the proof. Include the changing state in the model and reconsider the transformation before using this function equivalence to reorganize the work.

MATH.12:5.3 - Extract a case decision and its answer

For a rational input r=p/q, with integer p and positive integer q, construct either an indication that r=0 or a rational y such that r*y=1.

The proof examines the decidable integer condition p=0:

• If p=0, return Zero with the equality r=0.
• Otherwise return Inverse(q/p). Since p is nonzero, the fraction is defined, and (p/q)*(q/p)=1.

The result includes which case holds. At p=4,q=6 it returns Inverse(3/2). At p=0,q=5 it returns Zero. This tag lets a receiving calculation choose its continuation.

Merely reporting that one of the two conclusions holds loses the branch information the continuation needs. The construction obtains that information by testing an integer, then carries it with the result.

Now replace the rational representation by access to successively narrower rational intervals enclosing an arbitrary real number. The rational procedure’s test p=0 is no longer available. A nondegenerate rational interval containing zero does not by itself establish that the represented real is zero, because it also contains nonzero values. An interval [0,0] would establish equality, but the representation does not guarantee reaching such an interval. The previous proof does not supply a terminating zero test for this representation.

The next move is to obtain an appropriate decision procedure under additional input conditions, change the requested output to allow an unresolved case, or retain the existence conclusion without claiming the obtaining operation. The rational construction remains usable on its stated inputs.

MATH.12:6 - Bias-Annotation

A familiar proof can make its witness look obvious to an author while leaving a reader without the expression that produces it. Starting at the witness-introducing step exposes that omission.

A second bias is to treat logical existence, a computable selection and an efficient implementation as one result. The branch and function cases make their different requirements visible through changed inputs and repeated work.

MATH.12:7 - Conformance Checklist

1. The requested output and its relation to the input are stated.
2. Each data-consuming step has a supplied value or an obtaining operation.
3. Witness dependencies follow the statement’s quantifier order.
4. Pairs, projections, functions and case tags retain what the next step consumes.
5. Every claimed executable branch has its decision, and a terminating construction has the needed computation argument.
6. The selected representation exposes the required data. An executable construction has an available procedure for every choice used to produce its data.
7. The extracted expression produces the worked result under the original relation.
8. A changed premise returns to its affected construction and receiving uses.

Recognition can recover one witness-producing step. Assurance of the general obtaining operation examines the dependencies and computation rules needed for that claim.

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

MATH.12:9 - Consequences

The proof becomes usable for obtaining an object and for locating what changes when its premises change. Its constructive parts can be composed or assigned to different contributors through their stated inputs and outputs.

The recovered operation may be inefficient or depend on an unavailable decision. These are specific construction or implementation questions, which can be pursued while retaining the logical result already established.

MATH.12:10 - Architectural Rationale

The central move reads object production through the structure of a proof. Function application, pairing and case analysis let a receiver carry the proof’s intermediate results into the wanted output. Their computation rules explain why simplifying the construction preserves that output.

Inductive witness construction is one contributor. Recovering and assembling the computational content of an arbitrary supported argument also involves non-inductive steps, as the arithmetic identity and function equivalence show.

The correspondence between proofs and programs depends on the logic, data representation and evaluation rules. Keeping those choices explicit makes the connection usable: one can recover a mathematical construction, choose an implementation and then ask how it operates in the receiving subject.

MATH.12:11 - SoTA-Echoing

Adopt the proof/construction correspondence explained by Philip Wadler in Propositions as Types, especially §3 and the paired proof and computation rules in §§6-7. Its useful contribution here is to reconstruct operations from proof structure rather than treat a logical consequence as a finished obtaining procedure. Sections :4.2-:4.3 and the function case use that distinction. The selected correspondence concerns a stated logic and typed computation; a different calculus can require different rules. Author’s paper.

Use Egbert Rijke’s Introduction to Homotopy Type Theory, §2.2 and §4.6, for function application and dependent pairs with their projections. These give :4.3 a way to retain the witness together with its dependent property. The pattern presents those constructions without requiring the broader univalent foundation. Book.

Compare current Lean’s Axioms and Computation with a blanket interpretation of every existence proof as executable witness production. Its distinction between proof erasure, computation and classical choice changes :4.4: trace the data-producing operation and the evaluation actually claimed. Classical reasoning can remain in a correctness argument for an independently computable function. Lean documentation.

For an implementation using program extraction, Rocq’s Program extraction explains how logical content, informative axioms and supplied realizations affect the extracted code. This supports checking the actual extraction assumptions rather than reading a successful proof as validation of arbitrary inserted implementation code. Such implementation work becomes useful when the receiver needs executable code; it is not required for the hand calculations here. Rocq 9.1 documentation.

Reopen the chosen method when a needed proof rule has no available computational interpretation, a representation prevents a required decision, a source result changes that limit, or a more affordable construction provides the same wanted output.

MATH.12:12 - Relations

• B.5.RA recovers an argument’s premises and consequences. This pattern obtains the values and operations carried by its constructive steps.
• MATH.4 constructs witnesses by induction; MATH.5 extends assignments through mathematical composition. Their results can supply operations used in the extracted construction.
• MATH.2 governs independence from identified input descriptions; MATH.7 transports a construction through a bijection.
• MATH.9 constructs a choice compatible with symmetry. Its existence and computation conditions remain relevant when the extracted result includes such a choice.
• B.5.RR revises an affected argument; B.5.QD develops a missing construction into the next mathematical question.
• C.29.1 supplies a needed result-transfer argument; C.29.2 develops a missing computational formulation; C.29.3 connects a computation with its execution and interpreted result.

MATH.12:End

MATH.6 - Refute a Mathematical Claim with a Countermodel

Type: Method Status: Stable Normativity: Normative

MATH.6:1 - Problem frame

Use this pattern when a proposed mathematical implication might fail and you need a construction that settles the failure. Examples include a claimed property of every relation of a certain kind, a proposed inverse, or an interchange of quantifiers that would make a result more useful.

A countermodel gives mathematical objects, operations or relations in which the assumptions hold and the proposed conclusion fails. A counterexample to a statement about fixed objects supplies the particular values that make it fail. Both let you stop trying to prove the original claim and identify a useful change of question or assumptions.

Start by stating what must remain true and what would defeat the conclusion. Then construct one such case. Return the case and its decisive calculation or argument. A familiar counterexample already satisfying the present assumptions can finish the work immediately.

The reader needs elementary sets, relations, functions and quantified statements. The constructions below use ordinary mathematical truth and explicit witnesses; symbolic logic notation is explained where it changes the construction. A proof of a true claim, an estimate of how often a procedure fails, and an observation about a physical system require their corresponding methods. Countermodel construction answers whether the stated mathematical assumptions force the conclusion.

MATH.6:2 - Problem

Several successful examples can hide the condition on which a conclusion depends. Conversely, an apparently failing example can violate an assumption, use different arithmetic, or assign inconsistent values to one object. It then leaves the proposed implication unanswered.

The working difficulty is to keep the assumptions and the failed conclusion in one construction. Quantifier order determines which choices may depend on which inputs. The carrier and operation rules determine whether the proposed objects are admissible. Search limits determine what can be concluded when no failure is found.

MATH.6:3 - Forces

MATH.6:4 - Solution

State the implication → construct its failure condition → realize the objects and rules → establish assumptions and failure together → use the result or change the search.

MATH.6:4.1 - Recover the mathematical claim

Name the carrier sets, constants, operations and relations that may vary. Retain the restrictions already given: total or partial operations, finite or infinite carriers, allowed values, and any equations or other assumptions. Expand a definition when its content determines the case you need to build.

Write the proposed implication in the form “under these assumptions, this conclusion holds.” Keep a definition or assumption separate from the conclusion being tested. For example, adding transitivity to the assumptions would remove all nontransitive relations from a test of whether reflexivity and symmetry imply transitivity.

If the claim comes from another practice, first recover its mathematical formulation and the intended interpretation through FPF C.29. The mathematical countermodel will test that formulation. Its consequence for the practice depends on that correspondence.

MATH.6:4.2 - Work out what failure requires

Keep the assumptions true and negate the conclusion. Preserve the order and permitted dependence of choices. The following ordinary forms cover common starting points; P and R denote the stated properties, and each variable keeps its declared domain.

An equation between operations can often be defeated by one input tuple. Failure of transitivity requires three elements with the first two links present and the third absent. Start with those witnesses and use them to constrain the construction.

Where failure contains a universal requirement, give its argument or a complete finite case distinction. Finding one unsuccessful candidate for an existential conclusion leaves the other candidates open.

MATH.6:4.3 - Build objects that can realize the failure

Choose a familiar structure or a small carrier that has room for the required witnesses. Assign the constants and the critical relation entries or operation values first. Fill the remaining entries so that the assumptions continue to hold. Total operations need an output for every allowed input; partial operations retain their domains of definition.

For a finite relation, a table can make the critical choices visible. For a function, give its value at each element or give a defining rule. If the objects are classes of expressions, ensure the operation has the same value for equivalent representatives; MATH.2 supplies that construction.

Use the assumptions to reduce the choices. Symmetry determines the reversed relation entry; an identity law determines part of an operation table. After a forced assignment, return to any assumption that uses the changed entry. A conflict means this attempted construction needs revision.

Try a larger carrier or another kind of structure when the failure condition needs it. Smallness is useful for discovery and explanation; a smallest countermodel is required only when its minimality answers the question. A symbolic construction can cover an infinite carrier without listing its elements.

A model finder can supply assignments when the interacting constraints make manual construction expensive. Give it the assumptions together with the negated conclusion and the chosen search scope. Retain the meaning of its types, arithmetic and undefined values when interpreting the returned assignment.

MATH.6:4.4 - Establish that the construction defeats the claim

Evaluate every assumption used by the implication in the constructed case. Then exhibit the false conclusion with the witnesses or quantified argument from :4.2. These two parts establish the countermodel.

For a finite carrier, universal premises can be checked over all relevant tuples. For an infinite carrier, use a rule and an argument covering the required inputs. A program’s finite output can help discover that rule; the argument determines the wider conclusion.

If a search tool used a restricted interpretation, substitute its proposed counterexample back into the intended mathematical definitions. For example, a truncated representation of the natural numbers needs its missing values accounted for. Repair an assignment that relies on an unavailable value or an altered operation before using it to refute the original statement.

Suppose the source claim is n+1≠0 for natural numbers. An encoding instead uses addition modulo 2 and returns n=1. Its 1+1=0 becomes 1+1=2 in the source arithmetic, so this assignment fails to refute the source claim. Restore the source arithmetic before continuing that search, or prove the claim directly from n+1≥1.

Remove dispensable elements or assignments when that makes the reason easier to see. After such a simplification, repeat the affected assumption and failure checks. Keep a larger readable case if further minimization adds work without helping its use.

MATH.6:4.5 - Interpret an unsuccessful search

State what the search covered. Exhaustive failure to find a countermodel establishes absence only in the fully searched class and under the encoded semantics. A timeout or a partial enumeration leaves even that class unresolved.

When this absence is unexpected, compare the encoded assumptions with the intended ones. A contradictory or overrestrictive premise set can exclude the very cases under examination. Constructing one model of the assumptions alone can help distinguish that problem from an unsuccessful search for failure.

Choose the next move from what could answer the question: a different carrier, a symbolic infinite construction, a proof of the proposed claim, a weaker conclusion, or stopping with the searched-scope result. FPF C.11.DUA helps decide whether further inquiry is worth its cost. Enlarging the search is one option.

MATH.6:4.6 - Use the failure to revise the mathematical work

Return the assumptions that survived, the failed consequence, and the construction that separates them. This can reject an identification, stop an invalid proof attempt, expose a needed input, or identify an operation for which a proposed representation is unsuitable.

A repair is a new mathematical question. Restrict the domain, strengthen a justified premise, weaken the requested conclusion, or change the construction according to what the receiving work needs. Establish the revised claim on that scope; merely excluding the exhibited case can leave other failures.

Use B.5.RR to follow the effect through an existing argument. Use MATH.2 or MATH.5 when the affected step forms classes or interprets generating operations. Stop once the countermodel and its intended consequence are usable. No separate report form is needed for an ordinary calculation.

MATH.6:5 - Archetypal Grounding

MATH.6:5.1 - A relation that cannot serve as the proposed equivalence

The claim is that every reflexive, symmetric relation is transitive. On X={a,b,c}, assign the following relation; 1 means the pair is in the relation.

The diagonal establishes reflexivity. Matching entries across the diagonal establish symmetry. But a R b and b R c hold while a R c fails. This is a countermodel with the required three witnesses.

With at most two elements, every reflexive symmetric relation is transitive: in a two-link sequence x R y R z, either x=z, or one adjacent pair is an equal pair and the other link already supplies x R z. The third element makes the failure possible.

If the work needs the smallest equivalence relation containing this R, its transitive closure adds the missing pairs and gives the single class {a,b,c}. It answers whether elements are connected through R-links. A question about the original direct relation still needs the original table. For classes on which further operations must be defined, continue with MATH.2’s operation-preservation condition.

MATH.6:5.2 - A left inverse and the elements it does not recover

Consider the claim: if f:A→B has g:B→A with g(f(a))=a for every a, then f(g(b))=b for every b.

Choose A={u}, B={0,1}, f(u)=0, and g(0)=g(1)=u. Both maps are total. The premise holds at the only element of A, but f(g(1))=0. The claim fails because the left-inverse condition constrains recovery of source elements while B also contains an element outside the image of f.

Now require A and B to be the same finite set. The premise makes f injective: equality f(a)=f(a') gives a=a' after applying g. An injective self-map of a finite set is surjective. Write any b as f(a); then f(g(b))=f(g(f(a)))=f(a)=b. This supplies a proof for the changed domain.

For the same infinite set N={0,1,2,...}, take f(n)=n+1, g(0)=0, and g(n+1)=n. Then g(f(n))=n for every n, but f(g(0))=1. Every finite self-map search can miss this failure because the finite claim is true. The symbolic construction locates the lost premise: finiteness supplied the step from injection to surjection.

A receiving construction can retain the original left inverse for source recovery, require surjectivity for recovery of every target element, or restrict the target to the image. Which result is useful depends on the proposed representation.

MATH.6:5.3 - A separate answer for each input and one answer for all inputs

Let X=Y={0,1} and let R(x,y) mean x≠y. For every x there is a y satisfying R: choose y=1-x. The proposed stronger conclusion is that one y works for every x.

To defeat that conclusion, take any proposed y and choose x=y. Then R fails. This gives the required argument for both possible choices of y. It does not replace the premise’s input-dependent choice with a uniform one.

The useful result can instead be a function h(x)=1-x, satisfying R(x,h(x)) for every x. MATH.4 supplies inductive witness construction when a comparable task has finite inductively formed inputs and suitable base and constructor clauses. The countermodel identifies which input dependence the requested result must retain.

MATH.6:6 - Bias-Annotation

Small finite structures are prominent here because they expose the construction and make universal checks affordable. That preference can conceal infinite-only failures, as :5.2 demonstrates. The quantified claims also presuppose the stated mathematical interpretation; a probabilistic failure rate or empirical prevalence requires another question and method.

MATH.6:7 - Conformance Checklist

• The construction uses the domains, operation rules and assumptions of the claim being tested.
• The failure condition retains quantifier order and the allowed dependence of each choice.
• The proposed objects satisfy the assumptions and defeat the conclusion in the same interpretation.
• A finite search result states its covered scope; any wider conclusion has its own argument.
• The result changes the receiving proof, construction or question, with any proposed repair stated separately.

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

Put the desired conclusion among the assumptions. This excludes countermodels by construction. Keep the conclusion outside the retained assumptions, and inspect an unexpected empty search.

Use a failing case outside the stated domain. The infinite shift in :5.2 refutes the unrestricted self-map claim while the finite claim remains true. Carry the actual domain into the returned conclusion.

Keep one witness while reversing quantifier order. The witness in :5.3 depends on the input. Preserve that dependence, or establish a uniform witness as a different result.

Treat a search limit as the theorem’s limit. Recover which mathematical cases were represented. Change the construction or retain the bounded result when the desired claim reaches beyond them.

MATH.6:9 - Consequences

A countermodel gives a conclusive failure of the stated implication and a concrete object for further work. It can reveal a useful narrower theorem, a needed distinction, or a replacement construction. Its direct result is refutation on the stated interpretation; choosing and proving the repair remains further work.

An unsuccessful attempt can still identify an incompatible set of assignments or a limited class with no failure. Its usefulness depends on how that result changes the next mathematical move.

MATH.6:10 - Architectural Rationale

The method joins logical failure conditions with mathematical construction. Negating the conclusion tells the worker what to build; satisfying the assumptions makes the constructed case relevant; carrying the result back into the argument makes the criticism usable.

Separating these operations exposes two different errors: an inadmissible example and a failure condition that does not defeat the actual quantified claim. The finite and infinite inverse cases show how the same question can move between refutation and proof as the domain changes.

B.5.RA recovers an available argument, and B.5.RR revises reasoning when its premises or question change. This pattern supplies the mathematical countermodel they can consume. MATH.2’s failed-identification witness is a direct use, while the relation and inverse cases give this construction independent mathematical entries.

A known case or a short direct construction is preferable when it already settles the implication. Constraint solving helps when the assumptions interact enough to make that construction difficult. Neither route requires finding a smallest example unless its size matters to the receiving question.

MATH.6:11 - SoTA-Echoing

Question: how can a mathematical claim be refuted by a constructed interpretation while preserving its assumptions and quantifier dependencies?

Blanchette’s A User’s Guide to Nitpick for Isabelle/HOL, 18 January 2026, §§3.2-3.5, demonstrates carrier search, recovery of assigned constants, dependent witnesses and the treatment of infinite number types. Adopt those distinctions. The manual’s use of finite subsets for infinite types makes interpretation of a returned assignment important. The hand constructions here make the decisive reasoning accessible without requiring Isabelle.

The Alloy language reference, Commands specifies assertion checking as assumptions and declarations together with the negated assertion, within a scope. Adapt that construction to mathematical relations and operations; retain its distinction between assumptions, asserted consequences and search bounds. An empty search can expose an overrestricted formulation as well as an absence of counterexamples.

Direct construction, a supplied counterexample and a proof are meaningful alternatives at comparable effort. A model finder is useful when it supplies a difficult assignment, while symbolic reasoning remains important for quantified or infinite constructions. Reopen the chosen approach when a changed domain, equation or search interpretation changes what its result can establish.

MATH.6:12 - Relations

• Uses MATH.1 and MATH.2 when operations or classes are involved: construct permitted combinations and test whether the proposed identification preserves them.
• Connects with MATH.4: retain the dependence of a constructed witness on its input.
• Connects with MATH.5: a failed source equation can refute the proposed extension to identified expressions.
• Supplies B.5.RA and B.5.RR: use a mathematical failure in criticism and in revision of the affected argument.
• Uses C.29 for an external subject: establish what the mathematical failure means for that subject.
• Uses B.5.QD or C.11.DUA when continuation is the question: choose a worthwhile new problem or further inquiry from the result.

MATH.6:End

MATH.20 - Bound a Mathematical Unknown by Comparable Constructions

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

MATH.20:1 - Problem frame

Use this pattern when obtaining a mathematical value or object is difficult, but a justified comparison could already answer the receiving question. Construct something known to lie below, above, inside or outside the unknown in the relevant mathematical order.

Examples include bounding a best attainable value by a feasible construction and an inequality, enclosing a set between simpler sets, or converting an equation residual into a bound on solution error. The common method is to build and justify the comparison, then determine what it permits next.

First useful move: name the unknown and one comparison that would change the next action. A single feasible construction can settle an existence question or one side of an optimum bound. A proved enclosure can exclude a region. Construct only the bound the current question needs.

The reader needs elementary inequalities, sets and functions. The examples introduce their graph and set constructions; the residual example also uses linear equations and an inverse map. More specialized bounds require the properties of their particular mathematical objects.

If an available value or direct calculation answers the question more easily, use it. FPF’s characterization and choice methods select among alternatives; this pattern supplies mathematical bounds those choices may use. A mathematical comparison applied to a physical or organizational subject also requires the correspondence work in C.29 and MMP.

MATH.20:2 - Problem

A plausible estimate can be close in familiar cases while lying on the wrong side of an unknown elsewhere. A bound on an intermediate quantity can also be mistaken for a bound on the requested result. For example, a small equation residual need not imply a small error in its solution.

Bounds themselves can be uninformative. A wide interval may leave the receiving choice unchanged, and separately sharp coordinate bounds may never be attained together. The work needs both a justified relation and a way to tell whether improving that relation would help.

MATH.20:3 - Forces

MATH.20:4 - Solution

Local mantra: name the unknown and the needed comparison; construct a simpler comparator; prove its direction and scope; carry the comparison through the required operations; tighten or expose the gap; return the bounded result to use.

MATH.20:4.1 - Choose the quantity or object and its order

State what is unknown: a number, a function, a set, an error, an optimal value, or another mathematical object. State the comparison relation. Numerical order, pointwise order between functions and set inclusion support different conclusions.

For a numerical bound L≤q≤U, say which q is being bounded and under which assumptions. For an enclosure L⊆S⊆U, L consists of established members of S, while U contains every possible member under the stated description. Cardinality alone does not establish either inclusion.

For an optimum, distinguish the optimal value from an object attaining it. A bounded nonempty set of real values has an infimum and supremum, but an attaining object needs a further argument. For example, the interval (0,1) has infimum 0 and contains no minimum.

Select the needed direction and strength. To show q≤t, an upper bound at most t suffices. To refute that claim, a lower bound greater than t suffices. If the bounds straddle t, they leave this question open.

MATH.20:4.2 - Construct a comparator from available structure

Choose a construction whose relation to the unknown can be proved with available information.

Other constructions can use symmetry, a conserved quantity, a norm inequality or a comparison theorem. Select the property that supplies the missing direction. A familiar shape or similar-looking value is a candidate for investigation until that relation is established.

A comparator can be a different kind of object from the result. In :5.1 a node potential produces a numerical lower bound on every path length. The derivation makes those resulting values comparable; it does not compare a potential directly with a path.

MATH.20:4.3 - Establish the bound over its claimed domain

Prove the inequality or inclusion for every admitted case to which the result will apply. A feasible witness establishes one attainable value. A claim about all candidates needs a relation covering all of them, as the edge inequalities in :5.1 cover every path.

Track the assumptions used. For a relaxed feasible set, establish the original set’s inclusion in it and keep the objective unchanged on original candidates. For a norm estimate, specify the norm and the operator property that supports it. For a probabilistic inequality, retain its distributional conditions and probability claim.

Use a known comparison theorem when it settles this question. If it does not, MATH.19 can construct the missing intermediate inequality and MATH.6 can test a suspected overclaim with a separating case.

Where the comparison cannot be established, return the condition that is missing or the counterexample. A trial value may remain useful for exploration without being used as the unproved bound.

MATH.20:4.4 - Propagate the comparison through the needed operations

For an order-preserving map F, L≤q≤U implies F(L)≤F(q)≤F(U). For an order-reversing map, the endpoints exchange roles. Establish the relevant behavior on the admitted domain.

For example, multiplication by a nonnegative scalar preserves numerical order, while multiplication by a negative one reverses it. Squaring is increasing on nonnegative inputs; an interval crossing zero needs its minimum and maximum square computed on that interval. From -2≤x≤1, the bound is 0≤x²≤4.

For sets, image and preimage under a fixed function preserve inclusion; complement reverses it in a fixed ambient set. Thus an enclosure can be carried into a subsequent transformation without requiring the original set to be enumerated.

Keep shared variables and constraints when combining bounds. If x∈[0,1], separately bounding x and -x gives -1≤x+(-x)≤1, but retaining the dependency gives equality to zero. The loose result is valid; its loss comes from forgetting that the terms use the same x.

A bound computed with approximate arithmetic must preserve the claimed direction after that computation. A computational continuation can use error bounds or enclosing arithmetic for this purpose; the mathematical argument states the comparison it must maintain.

MATH.20:4.5 - Tighten the comparison or identify what prevents it

Inspect where the proof introduces slack. It may enlarge the feasible set, forget a dependency, replace a quantity by a worst-case value, or use one norm for effects that could be bounded separately.

Improve the part that can change the receiving result. Construct a better feasible candidate, strengthen the inequality, partition the domain, retain a lost relation, or add an available premise. A bound on a requested component can be enough when a bound on the whole object is costly or impossible.

Check attainability and equality conditions. When a feasible value meets a proved bound in the opposite direction, the optimum is established. When equality conditions conflict, the current bound can remain valid while failing to identify an attainable result. A sequence approaching a bound can establish an infimum or supremum without an attaining object.

If the gap reflects missing information, expose it. Two admissible constructions with different answers can show why the current assumptions do not determine a narrower result. That identifies a useful next assumption, observation or mathematical question.

MATH.20:4.6 - Use the bounded result and stop at the needed strength

Return the comparator, its relation to the requested result and the premises needed by the next use. A numerical interval, a set inclusion or a short inequality can carry this result.

For a minimization with feasible value U and lower bound L, the candidate is within U-L of the optimal value when these quantities are finite. The receiver can use that gap to decide whether further optimization matters. If only exclusion, existence or a threshold result was needed, stop once that result follows.

General choices about cost, value and further work use FPF’s existing characterization, Pareto and improvement methods. Componentwise mathematical bounds can inform them, but a candidate attaining one coordinate need not attain another. Preserve which constructions actually realize the compared results.

Reopen the affected bound when its domain, objective, available information or following operation changes. Preserve bounds whose proofs still apply.

MATH.20:5 - Archetypal Grounding

MATH.20:5.1 - Bound a shortest path before completing a search

Consider a finite directed graph with nonnegative edge weights and at least one path from s to t. Its shortest path length D is attained: cycles can be removed without increasing length, leaving one of finitely many simple paths.

Any particular s-to-t path of length U gives D≤U. For a lower bound, assign a number p(v) to each node such that, for every edge from u to v,

p(v)-p(u)≤w(u,v).

Along any path, add these inequalities. The intermediate potentials cancel, giving p(t)-p(s)≤path length. Therefore p(t)-p(s)≤D≤U.

Take nodes s,a,b,t and these edges:

The path s-a-t gives U=7. Choose p(s)=0, p(a)=2, p(b)=3, p(t)=4. The edge differences are respectively 2,2,3,1,1, each no larger than its edge weight. Thus 4≤D≤7.

The equality cases suggest s-a-b-t. It has length 4, meeting the lower bound, so D=4. The proof of optimality uses a feasible path and the comparison applying to every path; it does not need a list of every possible path.

Changed condition. Add an edge s-to-t of weight 1. The old potential violates its new edge inequality, since 4>1; its lower bound is invalid for the enlarged graph. The old path still supplies upper bound 4, and the new edge improves that to 1. The potentials p(s)=p(a)=p(b)=0, p(t)=1 satisfy every new edge inequality, proving D=1. Only the comparison affected by the new edge had to be replaced.

MATH.20:5.2 - Convert a residual to the error actually requested

Suppose Ax=b has an invertible linear map A, and an available approximation is xhat. Define its residual by r=A xhat-b. Then

xhat-x=A⁻¹r.

If the chosen vector norm and induced operator norm give ||A⁻¹||≤K, it follows that

||xhat-x||≤K||r||.

The bound K is the missing comparison between residual and solution error. It can come from a proved estimate of the inverse action; forming the entire inverse is unnecessary when a cheaper bound is available.

For a concrete case, A is diagonal with entries 1 and 0.001, b=(1,1), and xhat=(1,999). Use the maximum absolute coordinate as the vector norm. The inverse scales the coordinates by 1 and 1000, so its operator norm is 1000. The residual is (0,-0.001); the bound on solution error is 1. The actual solution (1,1000) attains that error.

A requested error of at most 0.01 therefore requires a residual bound of at most 0.00001 under this comparison. The apparent smallness of 0.001 was insufficient for that request.

Changed condition. Let the second diagonal entry become zero and b=(1,0). The equation fixes the first coordinate and leaves the second arbitrary. Residual zero cannot bound distance to a specified second-coordinate value: solutions with arbitrarily different second coordinates have the same residual. A request about the first coordinate alone is still answerable. Return that determined component or supply an additional condition selecting the second.

The method has derived an error relation and exposed its failure condition. A numerical method can now decide how accurately to obtain the residual and the approximation; the bound itself has not selected a solver.

MATH.20:5.3 - Enclose a set and improve the consequence

Let S be the disk {(x,y): x²+y²≤1}. The work needs the largest value of g(x,y)=x+y, but first seeks cheaper comparable sets.

The diamond L={(x,y): |x|+|y|≤1} lies inside S, because x²+y²≤(|x|+|y|)²≤1. The square U=[-1,1]×[-1,1] contains S, because each coordinate square is at most one. Thus L⊆S⊆U.

Over L, x+y≤|x|+|y|≤1, attained at (1,0). Over U, x+y≤2. Therefore the maximum over S lies between 1 and 2. Its existence follows, for example, from continuity of g on the compact disk.

The point (1,1) attaining the outer bound is outside S. To tighten that bound, retain the relation between the coordinates:

(x+y)²≤2(x²+y²)≤2,

where the first inequality follows from (x-y)²≥0. Hence x+y≤sqrt(2). The point (1/sqrt(2),1/sqrt(2)) belongs to S and attains this value, completing the comparison.

The inner set supplied feasible values; the outer set supplied a restriction on all feasible values. A better inequality and its equality case closed the gap. The same inclusion method can enclose a feasible region, a family of functions or another set, with the corresponding proof of membership and bound on the requested operation.

MATH.20:6 - Bias-Annotation

A single numerical answer can hide which object or property was bounded. The examples make that choice visible: path length, error in a vector, and an enclosed set with an objective on it.

Simple bounds can look weak beside a precise calculation, yet already settle the receiving question. A small displayed residual can produce the opposite bias. Judge the comparison by its proved relation to the needed result, keeping its cost in view.

MATH.20:7 - Conformance Checklist

For the comparison being used:

• The unknown, comparison relation and requested consequence are identifiable.
• A feasible witness, enclosing object or inequality supplies the claimed direction.
• The proof covers the domain and assumptions of the intended use.
• Operations preserve or reverse the comparison under stated conditions.
• Shared variables and dependencies are retained when their loss matters.
• The bound on a value is distinguished from an object attaining it.
• The remaining gap identifies either sufficient precision or a useful refinement.
• A changed premise reopens the comparison it invalidates, while unaffected results remain available.

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

One attainable value used as a universal bound in the wrong direction. A path of length 7 bounds the shortest length from above. The potential inequalities supply the lower bound.

The comparator’s optimizer used as an original solution. The square’s maximizing point in :5.3 is outside the disk. Check membership in the original feasible set before using it as a candidate.

An operation applied without its order conditions. Squaring an interval crossing zero requires inspecting zero and both endpoints; simply squaring endpoints in their original order gives the wrong enclosure.

A discrepancy used as the requested error. In :5.2 the inverse action amplifies the residual, and singularity removes the full-solution bound. Derive the relation or restrict the requested output.

Separate extrema treated as jointly attainable. Retain the common variables and equality conditions. Their incompatibility can explain why a valid bound remains loose.

MATH.20:9 - Consequences

A justified bound can terminate a search, establish an impossibility, support a controlled approximation or identify missing information. It can also make a difficult problem workable before its complete solution is available.

The constructions reveal further methods: improve a feasible witness, solve a relaxation, exploit a dependency or change the requested output. The comparison provides a reason to choose among these next mathematical operations.

MATH.20:10 - Architectural Rationale

The unknown is reached through another construction whose mathematical relation to it is tractable. Feasible witnesses, potential inequalities, inverse-map estimates and set inclusions give different ways to establish that relation. Their common structure is an order with a proved direction and operations that preserve the intended consequence.

Constructing bounds and choosing between alternatives have different results. The first supplies an inequality or enclosure; the second uses it with the purposes and costs of the work. This lets the same mathematical method serve proofs, computations and modeling without adding a separate preference system.

The gap is itself useful mathematical information. Matching attainable bounds can establish an optimum; a failed equality condition or two separating cases can show what prevents a narrower answer.

MATH.20:11 - SoTA-Echoing

The working question is how to obtain a useful justified comparison without first solving the whole problem. The selected line combines feasible construction, relaxation or a comparison identity with explicit order propagation and an examination of the remaining gap.

Vandenberghe’s Duality, EE236A lecture 6, especially 6-4 derives the relation between feasible primal and dual values. Its contribution to :4.2/:5.1 is that a feasible construction and a general inequality can bound the same optimum from opposite sides. A complete optimal solution is unnecessary for each bound. Direct solution is cheaper for an easy instance; bounding becomes useful when a partial construction already settles the receiving question. Equality and attainment require the particular argument, not an unrestricted assumption of strong duality.

Higham’s What Is Backward Error? and What Is a Condition Number? explain why a discrepancy must be combined with the relevant sensitivity and why norm, perturbation class and requested output matter. The adopted consequence is :4.3/:5.2: derive a bound for the requested error and inspect the inverse action. A bare residual is a cheaper observable but can answer a different question. A proved componentwise or structure-specific estimate can be more informative than a coarse whole-vector estimate; no one condition number is imposed on every problem.

The current Mathematics in Lean treatment of monotonicity and set inclusion makes the quantified preservation steps explicit. It supports :4.3-.4 and the set branch of :5.3. These mechanisms are usable in ordinary proofs or formal checking; choosing Lean is optional.

The synthesis retains the cheapest comparison that supports the requested result and exposes the part of its proof that could be tightened. Reopen it when the domain, objective, available premises or required operation changes, or when a different bound would resolve a still-open use with less work.

MATH.20:12 - Relations

• MATH.19 constructs the intermediate inequality or inclusion; MATH.6 separates a claimed bound from a counterexample.
• MATH.11 develops invariants that can constrain the unknown; MATH.17 helps analyze operations used to propagate comparisons.
• MATH.21 uses bounds to construct limits and obtain sufficient finite approximations.
• C.29 and MMP connect the mathematical comparison to the modeled subject.
• Computational methods can use these results in search exclusions, relaxation, approximation and resource analysis.
• FPF’s characterization, Pareto and improvement methods use the resulting comparisons to choose the next work.

MATH.20:End