Axiom audit

A guarded audit that the target theorem Oseledets.oseledets_filtration and its companion corollaries depend only on Lean/Mathlib's three standard axioms propext, Classical.choice, Quot.sound — in particular on no sorryAx and no extra axioms.

Each #guard_msgs in #print axioms block below compares the declaration's axiom set against the expected [propext, Classical.choice, Quot.sound] and fails the build if it ever differs, so this module is a continuously-checked regression test rather than an informational dump (it produces no output on success).

Issue #19 — the chaotic Bernoulli-suspension flow object

(positive metric entropy + a non-uniform ergodic invariant measure on which D_q is q-dependent)

Issue #19 — ergodicity of the constant-roof Bernoulli suspension flow

(the full ℝ-flow is ergodic iff the base shift is; its time-1 map is honestly NOT ergodic)

Issue #19 ext — two-sided Bernoulli ergodicity (keystone) + UNCONDITIONAL flow ergodicity

Issue #20 — two-sided / invertible Kolmogorov–Sinai generator theorem

(keystone), the two-sided-generating Bernoulli partition, the system-entropy unlock ksEntropy(bernZ) = Hnu, and the constant-roof suspension StandardBorelSpace.

Issue #20 fibre — product/skew entropy h(T×id)=h(T) (Walters Thm 4.23) and the

unconditional Category-C unlock: the constant-roof Bernoulli suspension time-1 map has metric entropy Hnu.

Issue #23 — finite-dimensional operator entropy (foundations)

DensityMatrix / vonNeumannEntropy, the partial trace as a positive trace-preserving map, the Kronecker spectrum, and the scalar Klein inequality.

Issue #23 assembly — von Neumann entropy additivity & subadditivity, and the DensityMatrix-level Kronecker / partial-trace maps.

Issue #23 — Left-handed partial-trace mirror guards (symmetry with the Right-handed ones).