Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

ProductPrefixRigidity

Abstract

For locally informationally complete normalized common-label source families, assuming label-independent norm products at every prefix, actual local compositions with isometric roots, one actor at each step, and inactive identity up to coordinate equivalence force positive prefixes to factor into scaled local isometries. A first zero factor annihilates the product map and all later products, without requiring other zero-tail factors to have scalar Grams.

Theorem 1.1 (prefix rigidity).

Lean statement: D5/S3/Quantum/Recovery/ProductPrefixRigidity.prefix_rigidity

Proof. Machine-checked in Lean as D5/S3/Quantum/Recovery/ProductPrefixRigidity.prefix_rigidity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For locally informationally complete normalized common-label source families, label-independent norm products along actual local compositions force positive prefixes to factor into scaled local isometries. A first zero factor annihilates the product map and all later products, without requiring other zero-tail factors to have scalar Grams.

References