Proof of `Joint reference image caps across both signs and all draws` (1st statement)
groundedproofs/Lax342547Proofs/ReferenceImages.lean · lax-342547
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Reindex the independent raw draws by component and multiply their exact image bounds. Both tuple dimensions and ranks may vary arbitrarily with the component. This gives the finite reference cap with every rank and conditioning cost explicit, before the final parameter payment.