MATH.2:4 - Solution
Local mantra: choose what may be identified; test the operations; repair the distinction; form the classes; answer only what those classes determine.
MATH.2:4.1 - Specify the carrier, operations and receiving question
Name the set A of objects and the operations to retain. An n-ary total operation f maps every tuple in A^n to an element of A. A partial operation has a stated domain D_f⊆A^n.
When an operation takes inputs from different sets or returns a result in another set, choose an equivalence relation on each participating set. Compare corresponding inputs under their sets’ relations and the resulting outputs under the output set’s relation. A transition on states and concatenation of paths are different operations; choose the one actually used by the proposed identification.
State the receiving question. For example, the receiver may need the parity of a sum, the cost of a continuation, or whether a next step is available. This determines which distinctions a useful quotient can lose.
MATH.2:4.2 - Make the proposed equality into an equivalence relation
Write a~b for the proposed identification. An equivalence relation is reflexive, symmetric and transitive. Its class [a] contains all objects identified with a; these classes partition A.
If the candidate is a resemblance, test the missing law before forming classes. For instance, on integers a~b defined by |a-b|≤1 is reflexive and symmetric but fails transitivity: 0 is related to 1 and 1 to 2, while 0 is not related to 2.
You can refine a proposed relation by retaining an additional property. Requiring both a~b and h(a)=h(b) remains an equivalence relation when ~ was one. Choose h from the failure that matters to the operation or query. The repaired relation still needs the operation test.
MATH.2:4.3 - Test compatibility, including the domain of a partial operation
For a total operation f, compare tuples whose corresponding entries are equivalent. The compatibility condition is:
a1~b1, …, an~bn ⇒ f(a1,…,an)~f(b1,…,bn).
An equivalence relation satisfying this condition for every retained total operation is a congruence for those operations.
For a partial operation, first require agreement about whether it can be applied:
a1~b1, …, an~bn ⇒ ((a1,…,an)∈D_f ⇔ (b1,…,bn)∈D_f).
Where both tuples are in the domain, require equivalent outputs as above. This pattern uses the resulting quotient convention in which availability is independent of the representative. A set-valued or approximate account that deliberately combines differing possibilities is another construction.
Use an algebraic argument for a general claim, or exhaustive checking when the specified carrier is finite. A few successful examples can suggest the relation; one failure is enough to refute compatibility.
If the test fails, keep the distinguishing information in the objects or narrow the operation/question being claimed. For a finite partition, split the failing class using the exposed distinction and retest the affected operations. This is a local repair; repeated splitting is not being offered here as a general minimization algorithm.
MATH.2:4.4 - Define the quotient operation and show that it is well defined
When the conditions hold, form A/~, the set of classes, and define the inherited operation by:
f_bar([a1],…,[an])=[f(a1,…,an)].
The right side is independent of the chosen representatives precisely because compatible inputs return equivalent outputs. For a partial operation, agreement of domains also makes its availability independent of that choice.
This argument is reusable for unchanged conditions. The useful result is an operation on classes, together with the relation and the reason it is valid. There is no need to reproduce the proof for every subsequent calculation with the same quotient.
Preserve a representative or a way to construct one when later work needs an individual object. Knowing only a class may be sufficient for one answer and insufficient for a later request about a member.
MATH.2:4.5 - Check which answers can be recovered and use the result
A value q(a) can be recovered from [a] when it is constant on that class: a~b ⇒ q(a)=q(b). Then define q_bar([a])=q(a). If this fails, return to the original objects, retain more information, or return the range of possibilities when that answers the question.
Use the quotient for the declared operations and answers. A new operation or query can require a finer relation. The old quotient retains its earlier use; revise the part that the new question distinguishes.
Stop with a valid class-level operation and usable answer, or with a counterexample identifying the lost operation or quantity. Additional formalization is useful only when it resolves a remaining mathematical or receiving question.