MATH.17:5 - Archetypal Grounding
MATH.17:5.1 - Individually permitted changes and a permitted whole
Let X={0,1} x {0,1}. An update is allowed to change at most one coordinate of each input pair. Flipping the first coordinate is allowed; flipping the second is allowed. Their composite sends (0,0) to (1,1) and changes two coordinates. The proposed collection is not closed under composition.
If the requirement limits each elementary step, keep a sequence of these steps and inspect intermediate states. If it limits the difference between initial and final states, test the composite against that bound and reject this pair. The same counterexample distinguishes the two intended uses.
Now take another requirement: the two coordinates must stay equal. Put P={(0,0),(1,1)} and admit functions sending P into P. The joint flip belongs; either single-coordinate flip fails. Closure follows from :4.3. This change of admissibility supplies a composable class suited to the equality requirement.
MATH.17:5.2 - Lift a rule, then change how repetition is distributed
Take integer operations f(n)=n+1 and g(n)=2n. Pointwise lifting to pairs is the case I={1,2}. Applied to (1,3), the lifted composite produces (4,8). Lifting f and g separately and then composing produces the same pair. The proof in :4.4 establishes that agreement for arbitrary inputs and functions.
Consider a different change: S(h)=h∘h, meaning repeat an operation twice. This always gives another integer endofunction, but the two sequencing proposals give:
S(g∘f)(n)=4n+6;
(S(g)∘S(f))(n)=4n+8.
At n=0 the answers are 6 and 8. To repeat the complete sequence, retain (g∘f)∘(g∘f). To run each stage twice, use g∘g∘f∘f. If f and g commute, rearrangement proves the two proposals equal; the present f and g do not.
The construction therefore returns both a valid operation on operations and a failed composition-preservation claim. That failure determines which changed rule implements the intended repetition.
MATH.17:5.3 - An operator whose useful law has another form
Let P=R[x], the real-coefficient polynomials in one variable, and define D:P -> P by differentiating each monomial: D(a*x^n)=n*a*x^(n-1) for n>0, and D(a)=0 for constants. This constructs an operation on functions through their polynomial expressions.
For p=x^2 and q=x+1:
D(p*q)=3*x^2+2*x.
The product of derivatives is D(p)*D(q)=2*x. The applicable law is instead:
D(p*q)=D(p)*q+p*D(q),
which gives the required result. To establish the law generally, first expand two monomials: differentiating a*b*x^(m+n) gives coefficient (m+n)*a*b, the sum of the two product-rule contributions. Distributing over the finite sums proves it for polynomials.
The same method of working is used as in :5.2: construct the operator, identify the law needed for the proposed use, and establish that law. Here it enables transforming a product expression into its derivative.
MATH.17:5.4 - Change a function while preserving its increments
Given a function f from the real numbers to the real numbers and a chosen point c, construct a function g that fixes c and preserves every increment of f. The requirements are g(c)=c and g(x)-g(y)=f(x)-f(y) for every x,y.
Set y=c in the second requirement. It forces g(x)=f(x)-f(c)+c. This defines a real-valued function; substituting c establishes the fixed point, and subtracting its values at x and y cancels the added constant and preserves the required increment. Thus the formula supplies the unique function under these requirements.
The transformation takes f itself as an input and returns g. Fixing a point and preserving increments do not settle an additional question about composition or cost. The repetition case in :5.2 shows how different requested changes lead to different operations on the same input rules.