"book-pflow-xyz/chapters/appendix-d-glossary.md" . . "Two nets compose by sharing a place, the way two tiles meet because their edges agree. No glue code is written to make them fit; the shared place *is* the interface. Invariants carry across in a specific sense: if a P-invariant of each component agrees with the other on the shared places, together they define a P-invariant of the composite — the theorem `invariant_lift`, kernel-checked in Lean ([`proofs/PflowProofs/InvariantLift.lean`](https://github.com/pflow-xyz/book-pflow-xyz/blob/main/proofs/PflowProofs/InvariantLift.lean)). A component's invariant extended by zeros is not in general an invariant of the composite, and liveness does not carry across at all (Appendix E; Chapters 4, 21; *A Tiling for Computation*)."@en . . "Edge-matching composition"@en . "4"^^ .