We establish a rigorously derived conservation law directly from calibrated astronomical imaging data.Given a family of linear observables on a Hilbert space of images, the induced feature matrix is shown to admit a non-trivial nullspace whenever rank deficiency occurs. This nullspace defines an invariant functional conserved across all observations. The result is formulated as the Truong Invariant Theorem and proven using operator theory and finite-dimensional linear algebra. The complete mathematical argument is provided in LaTeX and formally verified using Lean 4 with mathlib, ensuring machine-checked correctness. The framework is demonstrated on real JWST/M87 datasets and provides a reproducible pipeline for invariant discovery and data-driven conservation laws in astrophysical imaging. This archive contains:• the compiled paper (PDF)• full LaTeX source• formal Lean proof
Quoc Truong Nguyen (Fri,) studied this question.