MP-COMBINE-RESULTS - Change a rule so that separately obtained results can be combined
- Situation: A rule works for one input, but splitting the work or combining its results changes the answer.
- Question: What must each contribution retain, how should contributions combine, and why will the result still answer the original question?
- First useful result or blocker: A composable summary with a stated use. For an arithmetic mean of finitely many real values, return each group’s sum and count; add these pairs and divide the total sum by the total count.
- Start with: MATH.23 to develop the question; MATH.2 to choose compatible identification; MATH.17 to work on the combining operation; MATH.19 for the argument.
- Stop or return: Use the proved rule within its assumptions. A new statistic, allowed transformation or arithmetic implementation can invalidate a retained-information or proof step; return to that step.
Worked connection for MP-COMBINE-RESULTS
1. Recover the failure and intended result. Averaging the means of [0] and [2,4] gives 1.5, while the mean of the combined list is 2. MATH.23 turns this difference into a question: which summary recovers the mean of every nonempty combined finite list, for every partition into nonempty groups? The result is a claim and its range of cases for the identification step.
2. Decide what may be forgotten. MATH.2 tests identification against the operations still needed. Equal means are insufficient: [0] and [0,0] both have mean 0, but adjoining [2] gives means 1 and 2/3. Instead identify lists with equal sum and count. Concatenation respects that identification because both components add. Empty lists can have summary (0,0); division is defined only after the combined count is positive.
3. Make the rule itself available for work. Combine (s,n) and (t,m) as (s+t,n+m). MATH.17 asks whether the operation stays within the chosen space and which laws the use needs. The pair summarizes an input; the binary operation is another mathematical object, which can be compared with a replacement. Associativity permits regrouping; commutativity permits reordering. These laws become premises needed by the proof.
4. Connect the local calculation to all allowed combinations. MATH.19 separates two claims: summarizing a concatenation equals combining its summaries, and extracting s/n at positive n returns the list’s arithmetic mean. The first follows from addition of sums and lengths. Repeated combination follows by induction over the finite grouping, using MATH.4 if that induction needs construction. The argument thus covers every stated partition.
5. Use the result with its conditions. Contributors can now return pairs to combine. FPF C.29 connects the mathematics to actual records: which values belong to the population and whether any are duplicated remain subject questions. Real addition supplies the laws above; floating-point regrouping needs its numerical account when rounding can change the use.
6. Develop the next question. If the answer becomes a median, sum and count no longer suffice: [0,0,6] and [0,3,3] share both but have medians 0 and 3. Return to step 2 and use MATH.23 to construct the new question. A quantile method or a different summary can supply the next contribution.