Operator audit

Read side by side

An operator audit follows an operation through a change of description. It asks whether the new calculation performs the same task, which interactions it retains, and what evidence explains any difference. Use it when splitting an object into packets, changing coordinates, filtering a signal, or working from a summary.

Start here · Worked demonstrations · Glossary

Start with the matrix example below if this language is new. You can change its inputs and switch blocks on and off in the existing interactive diagram, or run and edit the packet program.

The audit in six questions

The answer can be exact agreement, a quantified difference, or an obstruction to the proposed task. Each is useful when its assumptions are explicit.

A complete audit of a two-coordinate operation

Specify the operation and the packets

Work with column vectors in \(\mathbb R^2\). Let

The two packets retain the first and second coordinates. They satisfy \(P_i^2=P_i\), \(P_1P_2=P_2P_1=0\), and \(P_1+P_2=I\). Thus \(x=P_1x+P_2x\). Direct multiplication gives \(Tx=(8,18)^{\mathsf T}\).

Account for all four transfers

The block \(P_jTP_i\) takes input from packet \(i\) to output packet \(j\). Rows name targets; columns name sources. Both diagonal and off-diagonal blocks belong to the operation.

Adding these contributions reproduces \((8,18)^{\mathsf T}\). The reason it works for every vector, beyond this particular input, is the operator identity

The packet demonstration gives the complete program, expected output, written-proof route, and recorded formal coverage.

Delete an interaction and identify the residual

Keep only the diagonal blocks. The resulting operation is

The omitted contribution is explicit:

Hence \(Tx=\widetilde T x+Ex\). The packets still reconstruct the input exactly; deleting their interactions changes the operation. In the interactive diagram, switch off the two off-diagonal blocks to reproduce this control. Switch them back on to restore the complete calculation.

Carry the operator through a coordinate change

If \(y=Cx\) with an invertible coordinate map \(C\), the same operation in the new coordinates has matrix \(T_y=CTC^{-1}\). The audit compares two routes:

For the same \(T\) and \(x\) above, choose

Then \(y=(5,3)^{\mathsf T}\) and both routes give \(T_y y=C(Tx)=(26,18)^{\mathsf T}\). Reusing the old matrix on \(y\) instead gives \(Ty=(11,27)^{\mathsf T}\), which fails this comparison. The coordinate walkthrough develops another example with every matrix product shown.

Invertibility matters here. When a representation discards information, there may be no \(C^{-1}\); a recovery question replaces this conjugation rule. For operations between different spaces, use the corresponding input and output coordinate maps. Check that every composition has matching types. The typed-path example explains why a one-sided inverse does not make both round trips identities.

Ask whether the retained information is sufficient

Suppose the available summary is \(R(x_1,x_2)=x_1+x_2\), while the requested answer is \(F(x_1,x_2)=x_1\). Exact recovery for every input would require a function \(G\) on the attainable summaries such that \(F=G\circ R\).

But \(u=(1,0)\) and \(v=(0,1)\) have \(R(u)=R(v)=1\), while \(F(u)=1\) and \(F(v)=0\). A single value \(G(1)\) cannot give both answers. This is an obstruction to every recovery function using that summary alone.

The same summary does recover \(H(x_1,x_2)=2x_1+2x_2\), using \(G_H(s)=2s\). Sufficiency depends on the question. Adding the measurement \(x_1-x_2\) also repairs the original task: if \(s=x_1+x_2\) and \(d=x_1-x_2\), then \(x_1=(s+d)/2\).

Open the Recovery Laboratory to change the measurement and the requested answer, inspect recovery rules or collision witnesses, and add missing information. The recovery demonstration supplies the elementary argument and its exact program.

Keep exactness, stability, and evidence separate

The block identity above is a finite linear-algebra calculation. More generally, let \(T:X\to Y\) be linear, with finite packet families \(P_i:X\to X\) and \(Q_j:Y\to Y\) whose sums are \(I_X\) and \(I_Y\). Then \(\sum_{j,i}Q_jTP_i=T\). The reconstruction follows by expanding \((\sum_jQ_j)T(\sum_iP_i)\).

When calling these maps packet projectors, also check their idempotence and the vanishing products within each family. Algebraic packet projectors can be oblique; these identities alone imply no norm-one or numerical-stability claim. Specify the norms, conditioning, and error model when those matter. Infinite decompositions additionally need a justified meaning for the sums and their convergence. Nonlinear operations require their own transfer laws.

An exact program can check a stated matrix identity or exhibit a failure witness. A finite sample of matching outputs alone establishes agreement on those inputs. For each broader conclusion, follow its written argument and retain its hypotheses. A linked Lean file or compilation record supports the formal statement and revision it actually checks.

These introductory calculations use classical linear algebra and the collection's existing examples. This guide adds an explanatory reading route; it does not change the recorded review or formal-verification status of a work.

Use the audit across the collection

A worksheet for your own operation

Copy these fields into your notes, then fill them for one concrete task:

Task and admissible inputs:
Input/output spaces and coefficients:
Operation and order of composition:
Representation and reconstruction maps:
Identity needed for the two routes to agree:
Retained blocks or measurements:
Residual, recovery rule, or failure witness:
Norms, approximation, and convergence assumptions, if used:
Argument, program, source revision, and tested scope:
Conclusion and remaining obligations:

Project map · All demonstrations · How to interpret verification