Joint linear information at a frontier

Let U and V be the spaces of linear observations available from the two sides. Their intersection is shared information. If observations P ≤ U and Q ≤ V are already exposed on the frontier, encode them together with that intersection. The modular identity below avoids charging the same information twice.

For a code generated by rows L_j, take U = span L_past, V = span L_future, and P,Q the visible rows on their respective sides. The rank formula then reads rank L_(past ∪ visible) + rank L_(future ∪ visible) - rank L. The affine-interface compiler instantiation is proved in the research note; these declarations check the underlying subspace identity and dimension formula.

theorem Complexity.Frontier.LinearBoundary.joint_eq {F : Type u_1} {W : Type u_2} [Field F] [AddCommGroup W] [Module F W] (U V P Q : Submodule F W) (hP : P ≤ U) (hQ : Q ≤ V) : U ⊓ V ⊔ (P ⊔ Q) = (U ⊔ Q) ⊓ (V ⊔ P)

Shared information and exposed observations form one subspace, not independent codes.

theorem Complexity.Frontier.LinearBoundary.finrank_joint {F : Type u_1} {W : Type u_2} [Field F] [AddCommGroup W] [Module F W] (U V P Q : Submodule F W) [FiniteDimensional F W] (hP : P ≤ U) (hQ : Q ≤ V) : Module.finrank F ↥(U ⊓ V ⊔ (P ⊔ Q)) = Module.finrank F ↥(U ⊔ Q) + Module.finrank F ↥(V ⊔ P) - Module.finrank F ↥(U ⊔ V)

The joint code can be smaller than the sum of the separate boundary and syndrome ranks.