Sin deriva en modelos functoriales para actualizaciones semánticas bajo gobernanza

Este documento formaliza y demuestra una propiedad de ausencia de deriva para sistemas que evolucionan bajo actualizaciones gobernadas. Los artefactos se modelan como funciones parametrizadas con comportamiento observable, y se requiere que las actualizaciones preserven la semántica a menos que se declaren explícitamente como cambios de contrato. Esto muestra que, bajo estas suposiciones, la equivalencia semántica es preservada y reflejada por todas las actualizaciones que no cambian el contrato, y que cualquier cambio en el comportamiento observable debe ocurrir mediante una actualización explícitamente gobernada. El resultado establece una garantía formal de estabilidad conductual en un modelo de despliegue controlado y está mecanizado en el demostrador de teoremas Lean. Véase https://github.com/AutonomicAI/equivalence-lean. Patente en trámite.