This preprint separates a narrow algebraic redundancy result from stronger claims about the Born rule and quantum ontology. Given finite nonnegative additive sector weights wγ, direct normalization already determines the probability law P (γ) = wγ / Ση wη. An optional Hilbert lift cγ = √wγ · e^iθγ reproduces the same law through Born normalization, so the Hilbert lift is probability-redundant once the sector weights are already supplied. The paper does not derive quantum mechanics from ℓ¹ structure. Instead, it proves and organizes finite algebraic results about normalization, scalar-ray invariance, support preservation, order preservation, disjoint-sector ℓ¹ additivity, phase-blind descent, row-sparsity of descent-compatible maps, and finite Local-Green/Global-Red quotient obstructions. The Lean4 hardening supports the finite rational kernels and witness examples, including Born-normalization redundancy and phase-sensitive mixing obstructions. The main firewall is that Born normalization redundancy is cheap algebra, while Born uniqueness and quantum-mechanical ontology require additional imported representation assumptions: Hilbert space, projection/frame-function structure, unitary dynamics, phase averaging, and measurement descent. The result is therefore an anti-overclaim note: local normalization lemmas are green, but global Born-rule ontology remains red unless those representation assumptions are explicitly supplied.
Jeremy H. Carroll (Sat,) studied this question.