renamed injections → injections_alg; defined new paper-style injections; top-level equivalence theorem statement