Coordinate Restriction Naturality

Abstract

Coordinate restriction preserves twisted diagonals for compatible value maps.

Theorem 1.1 (Coordinate restriction commutes with twisted diagonalization).

$$\forall A_i,A_j,Y_i,Y_j:\mathrm{Type},\forall iota:\mathrm{Embedding}\left(A_i,A_j\right),q:Y_j\to Y_i,ta{u}_j:Y_j\to Y_j,ta{u}_i:Y_i\to Y_i,E:A_j\to \left(A_j\to Y_j\right),(q\circ ta{u}_j=ta{u}_i\circ q)\Rightarrow \mathrm{restrictVector}\left(iota,q,\mathrm{diagonal}\left(ta{u}_j,E\right)\right)=\mathrm{diagonal}\left(ta{u}_i,\mathrm{restrictTable}\left(iota,q,E\right)\right).$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Naturality/CoordinateRestrictionNaturality.coordinate_restriction_naturality (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let Ai and Aj be address types, Yi and Yj be value types, iota embed Ai into Aj, and q map Yj to Yi. Restrict a table E by sending (a,b) to q(E(iota(a),iota(b))), and restrict a vector u by sending a to q(u(iota(a))).

For twists tauJ on Yj and tauI on Yi, assume q after tauJ equals tauI after q. Then restricting the tauJ-twisted diagonal of every table E equals the tauI-twisted diagonal of the restricted table. The proof evaluates the imported semiconjugacy equivalence at each diagonal entry.

Loogle and LeanSearch found Function.semiconj_iff_comp_eq for the exact intertwining hypothesis, and the Lean proof imports and applies it. Neither search found the full coordinate-restriction statement; repository and digestion-record searches found no duplicate.

References

• Truth anchor: D5/S0/Diagonal/Naturality/CoordinateRestrictionNaturality.coordinate_restriction_naturality
• Dependency: D5/S0/Diagonal/EscapeCount