TransferSpecification.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Independent specification of source lem:transfer / eq:rank-transfer. The fixed filter mask is arbitrary. Every remaining product coordinate and parity is averaged, and the actual nominal rank statistic is zero when unlisted.

def OAI.MatroidProphet.TransferClaim line 14
Source documentation
Full sample-to-rank contract for the actual rounded greedy survivor groups.
```
def TransferClaim : Prop :=
…
```