Let \(\mathcal C_a={\operatorname{im}} A_a\) and \(T_{ba}=A_bS_a\). Coordinate realizations are \(F_a=A_aFS_a\) on \(\mathcal C_a\). Both paths through the square represent the same underlying operation.
Read the diagram in words
The horizontal route applies the operation in a chart. The vertical route changes charts. Commutativity says that changing charts before or after the operation gives the same realizable coefficients. Agreement between charts does not by itself establish predictive accuracy.
Conversely, a compatible family \(G_a\) on the realizable coefficient spaces determines one operation. With a supplied reference chart \(r\),
The mathematical point
Compatibility is a descent condition: local coordinate descriptions belong to one object-space operation precisely when they agree under transport.
A fitted family's discrepancy can be measured in object space:
Scope
Zero chart discrepancy establishes agreement. It does not establish correctness of the agreed predictor. Deterministic recodings of the same observation supply the same observed information.
Formal route
Realization.lean. The formal construction uses a nonempty chart family.