3. Coordinate transport and one underlying operator
On this page · Permalink · Source line 63
For a nonempty atlas family, define transport on realizable coefficients from atlas \(a\) to atlas \(b\) by
For an endomorphism \(F:X\to X\), define its coordinate realization by \(F_a=A_aFS_a\) on \(\mathcal C_a\). In this paragraph \(F\) may be nonlinear. For a partial map, every formula is restricted to the transported admissible domain. Maps between different signal types use separate input and output atlases.
Proposition 2: Coherent transport and operator realization
On the consistent coefficient spaces,
Conversely, suppose maps \(G_a:\mathcal C_a\to\mathcal C_a\) satisfy \(G_bT_{ba}=T_{ba}G_a\) for every pair. Then there is a unique map \(F:X\to X\) with \(G_a=A_aFS_a\) for every \(a\).
Read proof · Recorded Lean scope · Visual guide: One operation, several coordinates · Permalink · Source line 73
Proof
The transport identities follow by inserting \(S_bA_b=I\). The operator identity follows because either path is \(A_bFS_a\). For the converse, choose a reference atlas \(r\) and put \(F=S_rG_rA_r\). Compatibility gives \(G_aA_a=A_aF\). Every consistent coefficient is \(A_ax\), which proves the asserted realization. Applying \(S_a\) proves uniqueness. \(\square\)
An independently fitted family of atlas predictors need not satisfy this proposition. Its compatibility residual is a well-defined quantity,
After synthesis it becomes an object-space discrepancy:
Thus \(\|S_bd_{ba}(x)\|\leq\|S_b\|\,\|d_{ba}(x)\|\). Zero discrepancy establishes that the chart descriptions agree, not that their common prediction is correct. All charts can agree on the same wrong operator.
Redundant coefficient outputs must also be tested for consistency. Synthesizing an arbitrary coefficient vector always produces some signal, but reanalysis returns \(\Pi_ac\), not necessarily the original \(c\). Reconstruction and coefficient consistency are different checks.