Proof of `Joint reference image caps across both signs and all draws` (2nd 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
Disintegrate the actual uniform raw law over its complete plus-frame observation. Each fiber is the independent product of the checked minus completion laws. Multiply its uniform joint-minus image bound by the plus-prescription probability and integrate. The result has factor 4^k and dimension loss k(d+h), uniformly over both nominal tuple ranks.